defpred S₁[ Function of MP-WFF,F₁(), Nat] means for A being MP-wff st card (dom A) <= $2 holds
( ( A = VERUM implies $1 . A = F₂() ) & ( for p being MP-variable st A = @ p holds
$1 . A = F₃(p) ) & ( for B being MP-wff st A = 'not' B holds
$1 . A = F₄(($1 . B)) ) & ( for B being MP-wff st A = (#) B holds
$1 . A = F₅(($1 . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
$1 . A = F₆(($1 . B),($1 . C)) ) );
defpred S₂[ Element of F₁(), Function of MP-WFF,F₁(), Element of MP-WFF ] means ( ( $3 = VERUM implies $1 = F₂() ) & ( for p being MP-variable st $3 = @ p holds
$1 = F₃(p) ) & ( for A being MP-wff st $3 = 'not' A holds
$1 = F₄(($2 . A)) ) & ( for A being MP-wff st $3 = (#) A holds
$1 = F₅(($2 . A)) ) & ( for A, B being MP-wff st $3 = A '&' B holds
$1 = F₆(($2 . A),($2 . B)) ) );
defpred S₃[ Nat] means ex F being Function of MP-WFF,F₁() st S₁[F,$1];
defpred S₄[ object , object ] means ex A being Element of MP-WFF st
( A = $1 & ( for g being Function of MP-WFF,F₁() st S₁[g, card (dom A)] holds
$2 = g . A ) );
A1: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis: ( S₃[k] implies S₃[k + 1] )
given F being Function of MP-WFF,F₁() such that A2: S₁[F,k] ; :: thesis: S₃[k + 1]
defpred S₅[ Element of MP-WFF , Element of F₁()] means ( ( card (dom $1) <> k + 1 implies $2 = F . $1 ) & ( card (dom $1) = k + 1 implies S₂[$2,F,$1] ) );
A3: for x being Element of MP-WFF ex y being Element of F₁() st S₅[x,y]

proof

let A be Element of MP-WFF ; :: thesis: ex y being Element of F₁() st S₅[A,y]

now :: thesis: ( ( card (dom A) <> k + 1 & ex y being Element of F₁() st verum ) or ( card (dom A) = k + 1 & A = VERUM & ex y being Element of F₁() st S₂[y,F,A] ) or ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p & ex y being Element of F₁() st S₂[y,F,A] ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B & ex y being Element of F₁() st S₂[y,F,A] ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B & ex y being Element of F₁() st S₂[y,F,A] ) or ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C & ex y being Element of F₁() st S₂[y,F,A] ) )

per cases ( card (dom A) <> k + 1 or ( card (dom A) = k + 1 & A = VERUM ) or ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) or ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ) by Th37;

case card (dom A) <> k + 1 ; :: thesis: ex y being Element of F₁() st verum

take y = F . A; :: thesis: verum

end;

case A4: ( card (dom A) = k + 1 & A = VERUM ) ; :: thesis: ex y being Element of F₁() st S₂[y,F,A]

take y = F₂(); :: thesis: S₂[y,F,A]
thus S₂[y,F,A] by A4, Lm4, Lm6; :: thesis: verum

end;

case ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) ; :: thesis: ex y being Element of F₁() st S₂[y,F,A]

then consider p being MP-variable such that
A5: A = @ p ;
take y = F₃(p); :: thesis: S₂[y,F,A]
thus S₂[y,F,A] by A5, Lm6, Th27, Th38; :: thesis: verum

end;

case ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) ; :: thesis: ex y being Element of F₁() st S₂[y,F,A]

then consider B being MP-wff such that
A6: A = 'not' B ;
take y = F₄((F . B)); :: thesis: S₂[y,F,A]
thus S₂[y,F,A] by A6, Lm4, Th28, Th38, Th39; :: thesis: verum

end;

case ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) ; :: thesis: ex y being Element of F₁() st S₂[y,F,A]

then consider B being MP-wff such that
A7: A = (#) B ;
take y = F₅((F . B)); :: thesis: S₂[y,F,A]
thus S₂[y,F,A] by A7, Lm4, Th29, Th38, Th39, Th40; :: thesis: verum

end;

case ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ; :: thesis: ex y being Element of F₁() st S₂[y,F,A]

then consider B, C being MP-wff such that
A8: A = B '&' C ;
take y = F₆((F . B),(F . C)); :: thesis: S₂[y,F,A]

now :: thesis: for B1, C1 being MP-wff st A = B1 '&' C1 holds
y = F₆((F . B1),(F . C1))

let B1, C1 be MP-wff; :: thesis: ( A = B1 '&' C1 implies y = F₆((F . B1),(F . C1)) )
assume A9: A = B1 '&' C1 ; :: thesis: y = F₆((F . B1),(F . C1))
then B = B1 by A8, Th30;
hence y = F₆((F . B1),(F . C1)) by A8, A9, Th30; :: thesis: verum

end;

hence S₂[y,F,A] by A8, Lm4, Th38, Th39, Th40; :: thesis: verum

end;

end;

end;

hence ex y being Element of F₁() st S₅[A,y] ; :: thesis: verum

end;

consider G being Function of MP-WFF,F₁() such that
A10: for p being Element of MP-WFF holds S₅[p,G . p] from FUNCT_2:sch 3(A3);
take H = G; :: thesis: S₁[H,k + 1]
thus S₁[H,k + 1] :: thesis: verum

proof

let A be Element of MP-WFF ; :: thesis: ( card (dom A) <= k + 1 implies ( ( A = VERUM implies H . A = F₂() ) & ( for p being MP-variable st A = @ p holds
H . A = F₃(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F₄((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F₅((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F₆((H . B),(H . C)) ) ) )
set p = card (dom A);
assume A11: card (dom A) <= k + 1 ; :: thesis: ( ( A = VERUM implies H . A = F₂() ) & ( for p being MP-variable st A = @ p holds
H . A = F₃(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F₄((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F₅((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F₆((H . B),(H . C)) ) )
thus ( A = VERUM implies H . A = F₂() ) :: thesis: ( ( for p being MP-variable st A = @ p holds
H . A = F₃(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F₄((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F₅((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F₆((H . B),(H . C)) ) )

proof

per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;

suppose card (dom A) <> k + 1 ; :: thesis: ( A = VERUM implies H . A = F₂() )

then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence ( A = VERUM implies H . A = F₂() ) by A2; :: thesis: verum

end;

suppose card (dom A) = k + 1 ; :: thesis: ( A = VERUM implies H . A = F₂() )

hence ( A = VERUM implies H . A = F₂() ) by A10; :: thesis: verum

end;

end;

end;

thus for p being MP-variable st A = @ p holds
H . A = F₃(p) :: thesis: ( ( for B being MP-wff st A = 'not' B holds
H . A = F₄((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F₅((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F₆((H . B),(H . C)) ) )

proof

let q be MP-variable; :: thesis: ( A = @ q implies H . A = F₃(q) )
assume A12: A = @ q ; :: thesis: H . A = F₃(q)

per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;

suppose card (dom A) <> k + 1 ; :: thesis: H . A = F₃(q)

then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F₃(q) by A2, A12; :: thesis: verum

end;

suppose card (dom A) = k + 1 ; :: thesis: H . A = F₃(q)

hence H . A = F₃(q) by A10, A12; :: thesis: verum

end;

end;

end;

thus for B being MP-wff st A = 'not' B holds
H . A = F₄((H . B)) :: thesis: ( ( for B being MP-wff st A = (#) B holds
H . A = F₅((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F₆((H . B),(H . C)) ) )

proof

let B be MP-wff; :: thesis: ( A = 'not' B implies H . A = F₄((H . B)) )
assume A13: A = 'not' B ; :: thesis: H . A = F₄((H . B))
then card (dom B) <> k + 1 by A11, Th33;
then A14: H . B = F . B by A10;

per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;

suppose card (dom A) <> k + 1 ; :: thesis: H . A = F₄((H . B))

then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F₄((H . B)) by A2, A13, A14; :: thesis: verum

end;

suppose card (dom A) = k + 1 ; :: thesis: H . A = F₄((H . B))

hence H . A = F₄((H . B)) by A10, A13, A14; :: thesis: verum

end;

end;

end;

thus for B being MP-wff st A = (#) B holds
H . A = F₅((H . B)) :: thesis: for B, C being MP-wff st A = B '&' C holds
H . A = F₆((H . B),(H . C))

proof

let B be MP-wff; :: thesis: ( A = (#) B implies H . A = F₅((H . B)) )
assume A15: A = (#) B ; :: thesis: H . A = F₅((H . B))
then card (dom B) <> k + 1 by A11, Th34;
then A16: H . B = F . B by A10;

per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;

suppose card (dom A) <> k + 1 ; :: thesis: H . A = F₅((H . B))

then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F₅((H . B)) by A2, A15, A16; :: thesis: verum

end;

suppose card (dom A) = k + 1 ; :: thesis: H . A = F₅((H . B))

hence H . A = F₅((H . B)) by A10, A15, A16; :: thesis: verum

end;

end;

end;

thus for B, C being MP-wff st A = B '&' C holds
H . A = F₆((H . B),(H . C)) :: thesis: verum

proof

let B, C be MP-wff; :: thesis: ( A = B '&' C implies H . A = F₆((H . B),(H . C)) )
assume A17: A = B '&' C ; :: thesis: H . A = F₆((H . B),(H . C))
then card (dom B) <> k + 1 by A11, Th35;
then A18: H . B = F . B by A10;
card (dom C) <> k + 1 by A11, A17, Th35;
then A19: H . C = F . C by A10;

per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;

suppose card (dom A) <> k + 1 ; :: thesis: H . A = F₆((H . B),(H . C))

then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F₆((H . B),(H . C)) by A2, A17, A18, A19; :: thesis: verum

end;

suppose card (dom A) = k + 1 ; :: thesis: H . A = F₆((H . B),(H . C))

hence H . A = F₆((H . B),(H . C)) by A10, A17, A18, A19; :: thesis: verum

end;

end;

end;

end;

end;

A20: S₃[ 0 ]

proof

set F = the Function of MP-WFF,F₁();
take the Function of MP-WFF,F₁() ; :: thesis: S₁[ the Function of MP-WFF,F₁(), 0 ]
let A be MP-wff; :: thesis: ( card (dom A) <= 0 implies ( ( A = VERUM implies the Function of MP-WFF,F₁() . A = F₂() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F₁() . A = F₃(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F₁() . A = F₄(( the Function of MP-WFF,F₁() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F₁() . A = F₅(( the Function of MP-WFF,F₁() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F₁() . A = F₆(( the Function of MP-WFF,F₁() . B),( the Function of MP-WFF,F₁() . C)) ) ) )
assume card (dom A) <= 0 ; :: thesis: ( ( A = VERUM implies the Function of MP-WFF,F₁() . A = F₂() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F₁() . A = F₃(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F₁() . A = F₄(( the Function of MP-WFF,F₁() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F₁() . A = F₅(( the Function of MP-WFF,F₁() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F₁() . A = F₆(( the Function of MP-WFF,F₁() . B),( the Function of MP-WFF,F₁() . C)) ) )
hence ( ( A = VERUM implies the Function of MP-WFF,F₁() . A = F₂() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F₁() . A = F₃(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F₁() . A = F₄(( the Function of MP-WFF,F₁() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F₁() . A = F₅(( the Function of MP-WFF,F₁() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F₁() . A = F₆(( the Function of MP-WFF,F₁() . B),( the Function of MP-WFF,F₁() . C)) ) ) by NAT_1:2; :: thesis: verum

end;

A21: for n being Nat holds S₃[n] from NAT_1:sch 2(A20, A1);
A22: for x being object st x in MP-WFF holds
ex y being object st S₄[x,y]

proof

let x be object ; :: thesis: ( x in MP-WFF implies ex y being object st S₄[x,y] )
assume x in MP-WFF ; :: thesis: ex y being object st S₄[x,y]
then reconsider x9 = x as Element of MP-WFF ;
consider F being Function of MP-WFF,F₁() such that
A23: S₁[F, card (dom x9)] by A21;
take F . x ; :: thesis: S₄[x,F . x]
take x9 ; :: thesis: ( x9 = x & ( for g being Function of MP-WFF,F₁() st S₁[g, card (dom x9)] holds
F . x = g . x9 ) )
thus x = x9 ; :: thesis: for g being Function of MP-WFF,F₁() st S₁[g, card (dom x9)] holds
F . x = g . x9
let G be Function of MP-WFF,F₁(); :: thesis: ( S₁[G, card (dom x9)] implies F . x = G . x9 )
defpred S₅[ Element of MP-WFF ] means ( card (dom $1) <= card (dom x9) implies F . $1 = G . $1 );
assume A24: S₁[G, card (dom x9)] ; :: thesis: F . x = G . x9
A25: for p being MP-variable holds S₅[ @ p]

proof

let p be MP-variable; :: thesis: S₅[ @ p]
assume A26: card (dom (@ p)) <= card (dom x9) ; :: thesis: F . (@ p) = G . (@ p)
hence F . (@ p) = F₃(p) by A23
.= G . (@ p) by A24, A26 ;
:: thesis: verum

end;

A27: for A, B being Element of MP-WFF st S₅[A] & S₅[B] holds
S₅[A '&' B]

proof

let A, B be MP-wff; :: thesis: ( S₅[A] & S₅[B] implies S₅[A '&' B] )
assume that
A28: ( S₅[A] & S₅[B] ) and
A29: card (dom (A '&' B)) <= card (dom x9) ; :: thesis: F . (A '&' B) = G . (A '&' B)
( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) ) by Th35;
hence F . (A '&' B) = F₆((G . A),(G . B)) by A23, A28, A29, XXREAL_0:2
.= G . (A '&' B) by A24, A29 ;
:: thesis: verum

end;

A30: for A being Element of MP-WFF st S₅[A] holds
S₅[ (#) A]

proof

let A be MP-wff; :: thesis: ( S₅[A] implies S₅[ (#) A] )
assume A31: S₅[A] ; :: thesis: S₅[ (#) A]
assume A32: card (dom ((#) A)) <= card (dom x9) ; :: thesis: F . ((#) A) = G . ((#) A)
card (dom A) < card (dom ((#) A)) by Th34;
hence F . ((#) A) = F₅((G . A)) by A23, A31, A32, XXREAL_0:2
.= G . ((#) A) by A24, A32 ;
:: thesis: verum

end;

A33: for A being Element of MP-WFF st S₅[A] holds
S₅[ 'not' A]

proof

let A be MP-wff; :: thesis: ( S₅[A] implies S₅[ 'not' A] )
assume A34: S₅[A] ; :: thesis: S₅[ 'not' A]
assume A35: card (dom ('not' A)) <= card (dom x9) ; :: thesis: F . ('not' A) = G . ('not' A)
card (dom A) < card (dom ('not' A)) by Th33;
hence F . ('not' A) = F₄((G . A)) by A23, A34, A35, XXREAL_0:2
.= G . ('not' A) by A24, A35 ;
:: thesis: verum

end;

A36: S₅[ VERUM ]

proof

assume A37: card (dom VERUM) <= card (dom x9) ; :: thesis: F . VERUM = G . VERUM
hence F . VERUM = F₂() by A23
.= G . VERUM by A24, A37 ;
:: thesis: verum

end;

for p being Element of MP-WFF holds S₅[p] from MODAL_1:sch 1(A36, A25, A33, A30, A27);
hence F . x = G . x9 ; :: thesis: verum

end;

consider F being Function such that
A38: dom F = MP-WFF and
A39: for x being object st x in MP-WFF holds
S₄[x,F . x] from CLASSES1:sch 1(A22);
rng F c= F₁()

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in F₁() )
assume y in rng F ; :: thesis: y in F₁()
then consider x being object such that
A40: ( x in MP-WFF & y = F . x ) by A38, FUNCT_1:def 3;
consider p being Element of MP-WFF such that
p = x and
A41: for g being Function of MP-WFF,F₁() st S₁[g, card (dom p)] holds
y = g . p by A39, A40;
consider G being Function of MP-WFF,F₁() such that
A42: S₁[G, card (dom p)] by A21;
y = G . p by A41, A42;
hence y in F₁() ; :: thesis: verum

end;

then reconsider F = F as Function of MP-WFF,F₁() by A38, FUNCT_2:def 1, RELSET_1:4;
consider A being MP-wff such that
A43: A = VERUM and
A44: for g being Function of MP-WFF,F₁() st S₁[g, card (dom A)] holds
F . VERUM = g . A by A39;
take F ; :: thesis: ( F . VERUM = F₂() & ( for p being MP-variable holds F . (@ p) = F₃(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F₄((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F₅((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F₆((F . A),(F . B)) ) )
consider G being Function of MP-WFF,F₁() such that
A45: S₁[G, card (dom A)] by A21;
F . VERUM = G . VERUM by A43, A44, A45;
hence F . VERUM = F₂() by A43, A45; :: thesis: ( ( for p being MP-variable holds F . (@ p) = F₃(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F₄((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F₅((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F₆((F . A),(F . B)) ) )
thus for p being MP-variable holds F . (@ p) = F₃(p) :: thesis: ( ( for A being Element of MP-WFF holds F . ('not' A) = F₄((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F₅((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F₆((F . A),(F . B)) ) )

proof

let p be MP-variable; :: thesis: F . (@ p) = F₃(p)
consider A being MP-wff such that
A46: A = @ p and
A47: for g being Function of MP-WFF,F₁() st S₁[g, card (dom A)] holds
F . (@ p) = g . A by A39;
consider G being Function of MP-WFF,F₁() such that
A48: S₁[G, card (dom A)] by A21;
F . (@ p) = G . (@ p) by A46, A47, A48;
hence F . (@ p) = F₃(p) by A46, A48; :: thesis: verum

end;

thus for A being Element of MP-WFF holds F . ('not' A) = F₄((F . A)) :: thesis: ( ( for A being Element of MP-WFF holds F . ((#) A) = F₅((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F₆((F . A),(F . B)) ) )

proof

let A be Element of MP-WFF ; :: thesis: F . ('not' A) = F₄((F . A))
consider A1 being MP-wff such that
A49: A1 = 'not' A and
A50: for g being Function of MP-WFF,F₁() st S₁[g, card (dom A1)] holds
F . ('not' A) = g . A1 by A39;
consider G being Function of MP-WFF,F₁() such that
A51: S₁[G, card (dom A1)] by A21;
A52: for k being Nat st k < card (dom ('not' A)) holds
S₁[G,k]

proof

let k be Nat; :: thesis: ( k < card (dom ('not' A)) implies S₁[G,k] )
assume A53: k < card (dom ('not' A)) ; :: thesis: S₁[G,k]
let a be Element of MP-WFF ; :: thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; :: thesis: ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) )
then card (dom a) <= card (dom ('not' A)) by A53, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) ) by A49, A51; :: thesis: verum

end;

A54: ex B being MP-wff st
( B = A & ( for g being Function of MP-WFF,F₁() st S₁[g, card (dom B)] holds
F . A = g . B ) ) by A39;
set k = card (dom A);
card (dom A) < card (dom ('not' A)) by Th33;
then S₁[G, card (dom A)] by A52;
then A55: F . A = G . A by A54;
F . ('not' A) = G . ('not' A) by A49, A50, A51;
hence F . ('not' A) = F₄((F . A)) by A49, A51, A55; :: thesis: verum

end;

thus for A being Element of MP-WFF holds F . ((#) A) = F₅((F . A)) :: thesis: for A, B being Element of MP-WFF holds F . (A '&' B) = F₆((F . A),(F . B))

proof

let A be Element of MP-WFF ; :: thesis: F . ((#) A) = F₅((F . A))
consider A1 being MP-wff such that
A56: A1 = (#) A and
A57: for g being Function of MP-WFF,F₁() st S₁[g, card (dom A1)] holds
F . ((#) A) = g . A1 by A39;
consider G being Function of MP-WFF,F₁() such that
A58: S₁[G, card (dom A1)] by A21;
A59: for k being Nat st k < card (dom ((#) A)) holds
S₁[G,k]

proof

let k be Nat; :: thesis: ( k < card (dom ((#) A)) implies S₁[G,k] )
assume A60: k < card (dom ((#) A)) ; :: thesis: S₁[G,k]
let a be Element of MP-WFF ; :: thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; :: thesis: ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) )
then card (dom a) <= card (dom ((#) A)) by A60, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) ) by A56, A58; :: thesis: verum

end;

A61: ex B being MP-wff st
( B = A & ( for g being Function of MP-WFF,F₁() st S₁[g, card (dom B)] holds
F . A = g . B ) ) by A39;
set k = card (dom A);
card (dom A) < card (dom ((#) A)) by Th34;
then S₁[G, card (dom A)] by A59;
then A62: F . A = G . A by A61;
F . ((#) A) = G . ((#) A) by A56, A57, A58;
hence F . ((#) A) = F₅((F . A)) by A56, A58, A62; :: thesis: verum

end;

thus for A, B being Element of MP-WFF holds F . (A '&' B) = F₆((F . A),(F . B)) :: thesis: verum

proof

let A, B be Element of MP-WFF ; :: thesis: F . (A '&' B) = F₆((F . A),(F . B))
set k1 = card (dom A);
set k2 = card (dom B);
consider A1 being MP-wff such that
A63: A1 = A '&' B and
A64: for g being Function of MP-WFF,F₁() st S₁[g, card (dom A1)] holds
F . (A '&' B) = g . A1 by A39;
consider G being Function of MP-WFF,F₁() such that
A65: S₁[G, card (dom A1)] by A21;
A66: for k being Nat st k < card (dom (A '&' B)) holds
S₁[G,k]

proof

let k be Nat; :: thesis: ( k < card (dom (A '&' B)) implies S₁[G,k] )
assume A67: k < card (dom (A '&' B)) ; :: thesis: S₁[G,k]
let a be Element of MP-WFF ; :: thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; :: thesis: ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) )
then card (dom a) <= card (dom (A '&' B)) by A67, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F₂() ) & ( for p being MP-variable st a = @ p holds
G . a = F₃(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F₄((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F₅((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F₆((G . B),(G . C)) ) ) by A63, A65; :: thesis: verum

end;

A68: ex B1 being MP-wff st
( B1 = A & ( for g being Function of MP-WFF,F₁() st S₁[g, card (dom B1)] holds
F . A = g . B1 ) ) by A39;
card (dom A) < card (dom (A '&' B)) by Th35;
then S₁[G, card (dom A)] by A66;
then A69: F . A = G . A by A68;
A70: ex C being MP-wff st
( C = B & ( for g being Function of MP-WFF,F₁() st S₁[g, card (dom C)] holds
F . B = g . C ) ) by A39;
card (dom B) < card (dom (A '&' B)) by Th35;
then S₁[G, card (dom B)] by A66;
then A71: F . B = G . B by A70;
F . (A '&' B) = G . (A '&' B) by A63, A64, A65;
hence F . (A '&' B) = F₆((F . A),(F . B)) by A63, A65, A69, A71; :: thesis: verum

end;