| ⊢ | w ∧ f ⊃ f1 ∧fin w1 | ChopRep | |
| ⊢ | w1 ∧ g ⊃ g1 | ||
| ⇒ ⊢ | w ∧ (f ; g) ⊃ (f1 ; g1) |
Proof:
1 | ⊢ w ∧ f ⊃ f1 ∧fin w1 | given |
2 | ⊢ w ∧ (f ; g) ⊃ (f1 ∧fin w) ; g | |
3 | ⊢ (f1 ∧fin w1) ; g ≡ f1 ; (w1 ∧ g) | |
4 | ⊢ w1 ∧ g ⊃ g1 | given |
5 | ⊢ f1 ; (w1 ∧ g) ⊃ f1 ; g1 | |
6 | ⊢ w ∧ (f ; g) ⊃ f1 ; g1 |
qed