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₂[ Function of MP-WFF ,F₁(), Element of 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 NAT ] means ex F being Function of MP-WFF ,F₁() st S₂[F,$1];
A1: S₃[ 0 ]

proof

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

end;

A3: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₃[k] implies S₃[k + 1] )
given F being Function of MP-WFF ,F₁() such that A4: 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] ) );
A5: 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

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 Th48;

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

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

end;

case A6: ( 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 A6, 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
A7: A = @ p ;
take y = F₃(p); :: thesis: S₁[y,F,A]
thus S₁[y,F,A] by A7, Lm6, Th37, Th49; :: 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
A8: A = 'not' B ;
take y = F₄((F . B)); :: thesis: S₁[y,F,A]
thus S₁[y,F,A] by A8, Lm4, Th38, Th49, Th50; :: 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
A9: A = (#) B ;
take y = F₅((F . B)); :: thesis: S₁[y,F,A]
thus S₁[y,F,A] by A9, Lm4, Th39, Th49, Th50, Th51; :: 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
A10: A = B '&' C ;
take y = F₆((F . B),(F . C)); :: thesis: S₁[y,F,A]

now

now

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

end;

hence S₁[y,F,A] by A10, Lm4, Th49, Th50, Th51; :: thesis: verum

end;

hence S₁[y,F,A] ; :: 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
A11: for p being Element of MP-WFF holds S₄[p,G . p] from FUNCT_2:sch 3(A5);
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 A12: 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 A13: card (dom A) <> k + 1 ; :: thesis: ( A = VERUM implies H . A = F₂() )

then A14: card (dom A) <= k by A12, NAT_1:8;
H . A = F . A by A11, A13;
hence ( A = VERUM implies H . A = F₂() ) by A4, A14; :: thesis: verum

end;

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

hence ( A = VERUM implies H . A = F₂() ) by A11; :: 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 A15: A = @ q ; :: thesis: H . A = F₃(q)

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

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

then A17: card (dom A) <= k by A12, NAT_1:8;
H . A = F . A by A11, A16;
hence H . A = F₃(q) by A4, A15, A17; :: thesis: verum

end;

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

hence H . A = F₃(q) by A11, A15; :: 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 A18: A = 'not' B ; :: thesis: H . A = F₄((H . B))
then card (dom B) <> k + 1 by A12, Th44;
then A19: H . B = F . B by A11;

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

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

then A21: card (dom A) <= k by A12, NAT_1:8;
H . A = F . A by A11, A20;
hence H . A = F₄((H . B)) by A4, A18, A19, A21; :: thesis: verum

end;

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

hence H . A = F₄((H . B)) by A11, A18, A19; :: 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 A22: A = (#) B ; :: thesis: H . A = F₅((H . B))
then card (dom B) <> k + 1 by A12, Th45;
then A23: H . B = F . B by A11;

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

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

then A25: card (dom A) <= k by A12, NAT_1:8;
H . A = F . A by A11, A24;
hence H . A = F₅((H . B)) by A4, A22, A23, A25; :: thesis: verum

end;

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

hence H . A = F₅((H . B)) by A11, A22, A23; :: 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 A26: A = B '&' C ; :: thesis: H . A = F₆((H . B),(H . C))
then card (dom B) <> k + 1 by A12, Th46;
then A27: H . B = F . B by A11;
card (dom C) <> k + 1 by A12, A26, Th46;
then A28: H . C = F . C by A11;

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

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

then A30: card (dom A) <= k by A12, NAT_1:8;
H . A = F . A by A11, A29;
hence H . A = F₆((H . B),(H . C)) by A4, A26, A27, A28, A30; :: 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 A11, A26, A27, A28; :: thesis: verum

end;

end;

end;

end;

end;

A31: for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A1, A3);
defpred S₄[ set , set ] 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 ) );
A38: for x being set st x in MP-WFF holds
ex y being set st S₄[x,y]

proof

let x be set ; :: thesis: ( x in MP-WFF implies ex y being set st S₄[x,y] )
assume x in MP-WFF ; :: thesis: ex y being set st S₄[x,y]
then reconsider x' = x as Element of MP-WFF ;
consider F being Function of MP-WFF ,F₁() such that
A39: S₂[F, card (dom x')] by A31;
take F . x ; :: thesis: S₄[x,F . x]
take x' ; :: thesis: ( x' = x & ( for g being Function of MP-WFF ,F₁() st S₂[g, card (dom x')] holds
F . x = g . x' ) )
thus x = x' ; :: thesis: for g being Function of MP-WFF ,F₁() st S₂[g, card (dom x')] holds
F . x = g . x'
let G be Function of MP-WFF ,F₁(); :: thesis: ( S₂[G, card (dom x')] implies F . x = G . x' )
assume A40: S₂[G, card (dom x')] ; :: thesis: F . x = G . x'
defpred S₅[ Element of MP-WFF ] means ( card (dom $1) <= card (dom x') implies F . $1 = G . $1 );
A41: S₅[ VERUM ]

proof

assume A42: card (dom VERUM ) <= card (dom x') ; :: thesis: F . VERUM = G . VERUM
hence F . VERUM = F₂() by A39
.= G . VERUM by A40, A42 ;
:: thesis: verum

end;

A43: for p being MP-variable holds S₅[ @ p]

proof

let p be MP-variable; :: thesis: S₅[ @ p]
assume A44: card (dom (@ p)) <= card (dom x') ; :: thesis: F . (@ p) = G . (@ p)
hence F . (@ p) = F₃(p) by A39
.= G . (@ p) by A40, A44 ;
:: thesis: verum

end;

A45: 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 A46: S₅[A] ; :: thesis: S₅[ 'not' A]
assume A47: card (dom ('not' A)) <= card (dom x') ; :: thesis: F . ('not' A) = G . ('not' A)
card (dom A) < card (dom ('not' A)) by Th44;
hence F . ('not' A) = F₄((G . A)) by A39, A46, A47, XXREAL_0:2
.= G . ('not' A) by A40, A47 ;
:: thesis: verum

end;

A48: 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 A49: S₅[A] ; :: thesis: S₅[ (#) A]
assume A50: card (dom ((#) A)) <= card (dom x') ; :: thesis: F . ((#) A) = G . ((#) A)
card (dom A) < card (dom ((#) A)) by Th45;
hence F . ((#) A) = F₅((G . A)) by A39, A49, A50, XXREAL_0:2
.= G . ((#) A) by A40, A50 ;
:: thesis: verum

end;

A51: 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
A52: S₅[A] and
A53: S₅[B] and
A54: card (dom (A '&' B)) <= card (dom x') ; :: thesis: F . (A '&' B) = G . (A '&' B)
A55: card (dom A) < card (dom (A '&' B)) by Th46;
card (dom B) < card (dom (A '&' B)) by Th46;
hence F . (A '&' B) = F₆((G . A),(G . B)) by A39, A52, A53, A54, A55, XXREAL_0:2
.= G . (A '&' B) by A40, A54 ;
:: thesis: verum

end;

for p being Element of MP-WFF holds S₅[p] from MODAL_1:sch 1(A41, A43, A45, A48, A51);
hence F . x = G . x' ; :: thesis: verum

end;

consider F being Function such that
A56: dom F = MP-WFF and
A57: for x being set st x in MP-WFF holds
S₄[x,F . x] from CLASSES1:sch 1(A38);
F is Function of MP-WFF ,F₁()

proof

rng F c= F₁()

proof

let y be set ; :: 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 set such that
A58: x in MP-WFF and
A59: y = F . x by A56, FUNCT_1:def 5;
consider p being Element of MP-WFF such that
p = x and
A60: for g being Function of MP-WFF ,F₁() st S₂[g, card (dom p)] holds
y = g . p by A57, A58, A59;
consider G being Function of MP-WFF ,F₁() such that
A61: S₂[G, card (dom p)] by A31;
y = G . p by A60, A61;
hence y in F₁() ; :: thesis: verum

end;

hence F is Function of MP-WFF ,F₁() by A56, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

then reconsider F = F as Function of MP-WFF ,F₁() ;
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 A being MP-wff such that
A62: ( A = VERUM & ( for g being Function of MP-WFF ,F₁() st S₂[g, card (dom A)] holds
F . VERUM = g . A ) ) by A57;
consider G being Function of MP-WFF ,F₁() such that
A63: S₂[G, card (dom A)] by A31;
F . VERUM = G . VERUM by A62, A63;
hence F . VERUM = F₂() by A62, A63; :: 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
A64: ( A = @ p & ( for g being Function of MP-WFF ,F₁() st S₂[g, card (dom A)] holds
F . (@ p) = g . A ) ) by A57;
consider G being Function of MP-WFF ,F₁() such that
A65: S₂[G, card (dom A)] by A31;
F . (@ p) = G . (@ p) by A64, A65;
hence F . (@ p) = F₃(p) by A64, A65; :: 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
A66: ( A1 = 'not' A & ( for g being Function of MP-WFF ,F₁() st S₂[g, card (dom A1)] holds
F . ('not' A) = g . A1 ) ) by A57;
consider G being Function of MP-WFF ,F₁() such that
A67: S₂[G, card (dom A1)] by A31;
A68: for k being Element of NAT st k < card (dom ('not' A)) holds
S₂[G,k]

proof

let k be Element of NAT ; :: thesis: ( k < card (dom ('not' A)) implies S₂[G,k] )
assume A69: 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 A69, 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 A66, A67; :: thesis: verum

end;

A70: F . ('not' A) = G . ('not' A) by A66, A67;
set k = card (dom A);
card (dom A) < card (dom ('not' A)) by Th44;
then A71: S₂[G, card (dom A)] by A68;
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 A57;
then F . A = G . A by A71;
hence F . ('not' A) = F₄((F . A)) by A66, A67, A70; :: 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
A72: ( A1 = (#) A & ( for g being Function of MP-WFF ,F₁() st S₂[g, card (dom A1)] holds
F . ((#) A) = g . A1 ) ) by A57;
consider G being Function of MP-WFF ,F₁() such that
A73: S₂[G, card (dom A1)] by A31;
A74: for k being Element of NAT st k < card (dom ((#) A)) holds
S₂[G,k]

proof

let k be Element of NAT ; :: thesis: ( k < card (dom ((#) A)) implies S₂[G,k] )
assume A75: 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 A75, 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 A72, A73; :: thesis: verum

end;

A76: F . ((#) A) = G . ((#) A) by A72, A73;
set k = card (dom A);
card (dom A) < card (dom ((#) A)) by Th45;
then A77: S₂[G, card (dom A)] by A74;
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 A57;
then F . A = G . A by A77;
hence F . ((#) A) = F₅((F . A)) by A72, A73, A76; :: 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))
consider A1 being MP-wff such that
A78: ( A1 = A '&' B & ( for g being Function of MP-WFF ,F₁() st S₂[g, card (dom A1)] holds
F . (A '&' B) = g . A1 ) ) by A57;
consider G being Function of MP-WFF ,F₁() such that
A79: S₂[G, card (dom A1)] by A31;
A80: for k being Element of NAT st k < card (dom (A '&' B)) holds
S₂[G,k]

proof

let k be Element of NAT ; :: thesis: ( k < card (dom (A '&' B)) implies S₂[G,k] )
assume A81: 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 A81, 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 A78, A79; :: thesis: verum

end;

A82: F . (A '&' B) = G . (A '&' B) by A78, A79;
set k1 = card (dom A);
set k2 = card (dom B);
card (dom A) < card (dom (A '&' B)) by Th46;
then A83: S₂[G, card (dom A)] by A80;
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 A57;
then A84: F . A = G . A by A83;
card (dom B) < card (dom (A '&' B)) by Th46;
then A85: S₂[G, card (dom B)] by A80;
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 A57;
then F . B = G . B by A85;
hence F . (A '&' B) = F₆((F . A),(F . B)) by A78, A79, A82, A84; :: thesis: verum

end;