Theorem 22

1. $\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle K_i\beta$.

(1)	$\langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle [F_i] K_i(\alpha\to \beta)$	(DE2), K$_t$4
(2)	$\langle F_i \rangle K_i(\alpha\to \beta) \to [F_i] \langle F_i \rangle K_i(\alpha\to \beta)$	(1), (TL3)
(3)	$\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \t... ...ngle F_i \rangle K_i\alpha \land [F_i] \langle F_i \rangle K_i(\alpha\to \beta)$	(2)
(4)	$\langle F_i \rangle K_i\alpha \land [F_i] \langle F_i \rangle K_i(\alpha\to \be... ... \langle F_i \rangle (K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta))$	K$_t$4
(5)	$\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle (K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta))$	(3), (4)
(6)	$K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle K_i\beta$	Th. 21
(7)	$\langle F_i \rangle (K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta)) \to \langle F_i \rangle \langle F_i \rangle K_i\beta$	(6), K$_t$4
(8)	$\langle F_i \rangle (K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta)) \to \langle F_i \rangle \langle F_i \rangle K_i\beta$	(5), (7)
(9)	$\langle F_i \rangle \langle F_i \rangle K_i\beta \to \langle F_i \rangle K_i\beta$	K$_t$4
(10)	$\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle K_i\beta$	(8), (9)

2. $\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle K_i(\alpha\land \beta)$

(1)	$\langle F_i \rangle K_i\beta \to \langle F_i \rangle [F_i] K_i\beta$	(DE2), K$_t$4
(2)	$\langle F_i \rangle K_i\beta \to [F_i] \langle F_i \rangle K_i\beta$	(1), (TL3)
(3)	$\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle K_i\alpha \land [F_i] \langle F_i \rangle K_i\beta$	(2)
(4)	$\langle F_i \rangle K_i\alpha \land [F_i] \langle F_i \rangle K_i\beta \to \langle F_i \rangle (K_i\alpha \land \langle F_i \rangle K_i\beta)$	K$_t$4
(5)	$\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle (K_i\alpha \land \langle F_i \rangle K_i\beta)$	(3), (4)
(6)	$K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle (K_i\alpha \land K_i\beta)$	Th. 21
(7)	$\langle F_i \rangle (K_i\alpha \land \langle F_i \rangle K_i\beta) \to \langle F_i \rangle \langle F_i \rangle (K_i\alpha \land K_i\beta)$	(6), K$_t$4
(8)	$\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle \langle F_i \rangle (K_i\alpha \land K_i\beta)$	(5), (7)
(9)	$\langle F_i \rangle \langle F_i \rangle (K_i\alpha \land K_i\beta) \to \langle F_i \rangle (K_i\alpha \land K_i\beta)$	K$_t$4
(10)	$\langle F_i \rangle K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle K_i\beta$	(8), (9)