Theorem 21

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

(1)	$K_i\alpha \to [F_i]K_i\alpha$	(DE2)
(2)	$K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to [F_i]K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta)$	(1)
(3)	$[F_i]K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle K_i\beta$	K$_t$4
(4)	$K_i\alpha \land \langle F_i \rangle K_i(\alpha\to \beta) \to \langle F_i \rangle K_i\beta$	(2), (3)

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

(1)	$K_i\alpha \to [F_i]K_i\alpha$	(DE2)
(2)	$K_i\alpha \land \langle F_i \rangle K_i\beta \to [F_i]K_i\alpha \land \langle F_i \rangle K_i\beta$	(1)
(3)	$[F_i]K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle K_i(\alpha\land \beta)$	K$_t$4
(4)	$K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle K_i(\alpha\land \beta)$	(2), (3)

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

(1)	$K_i\beta \to \langle F_i \rangle K_i\beta$	(MON$_{de}$)
(2)	$K_i\alpha \land K_i\beta \to K_i\alpha \land \langle F_i \rangle K_i\beta$	(1)
(3)	$K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle K_i(\alpha\land \beta)$	Th. 21.2.
(4)	$K_i\alpha \land K_i\beta\to \langle F_i \rangle K_i(\alpha\land \beta)$	(2), (3)

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

(1)	$K_i(\alpha \land \beta) \to \langle F_i \rangle K_i\alpha$	(MON$_{de}$)
(2)	$K_i(\alpha\land \beta) \to [F_i]K_i(\alpha\land \beta)$	(DE2)
(3)	$K_i(\alpha\land \beta) \to \langle F_i \rangle K_i\alpha \land [F_i]K_i(\alpha\land \beta)$	(1), (2)
(4)	$K_i(\alpha\land \beta) \to \langle F_i \rangle(K_i\alpha \land K_i(\alpha\land \beta))$	(3), K$_t$4
(5)	$K_i\alpha \to [F_i]K_i\alpha$	(DE2)
(6)	$K_i(\alpha\land \beta) \to \langle F_i \rangle K_i\beta$	(MON$_{de}$)
(7)	$K_i\alpha \land K_i(\alpha\land \beta) \to [F_i]K_i\alpha \land \langle F_i \rangle K_i\beta$	(5), (6)
(8)	$[F_i]K_i\alpha \land \langle F_i \rangle K_i\beta \to \langle F_i \rangle (K_i\alpha \land K_i\beta)$	K$_t$4
(9)	$K_i\alpha \land K_i(\alpha\land \beta) \to \langle F_i \rangle (K_i\alpha \land K_i\beta)$	(7), (8)
(10)	$\langle F_i \rangle(K_i\alpha \land K_i(\alpha\land \beta)) \to \langle F_i \rangle \langle F_i \rangle (K_i\alpha \land K_i\beta)$	(9), K$_t$4
(11)	$K_i(\alpha\land \beta) \to \langle F_i \rangle \langle F_i \rangle (K_i\alpha \land K_i\beta)$	(4), (10)
(12)	$K_i(\alpha\land \beta) \to \langle F_i \rangle (K_i\alpha\land K_i\beta)$	(11), K$_t$4

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

(1)	$K_i(\alpha\land \beta) \to \langle F_i \rangle (K_i\alpha\land K_i\beta)$	Th. 21.4.
(2)	$\langle F_i \rangle K_i(\alpha\land \beta) \to \langle F_i \rangle \langle F_i \rangle (K_i\alpha\land K_i\beta)$	(1), K$_t$4
(3)	$\langle F_i \rangle K_i(\alpha\land \beta) \to \langle F_i \rangle (K_i\alpha\land K_i\beta)$	(2), K$_t$4