defpred S1[ Element of F1(), Function of QC-Sub-WFF ,F1(), Element of QC-Sub-WFF ] means ( ( $3 is Sub_VERUM implies $1 = F2() ) & ( $3 is Sub_atomic implies $1 = F3($3) ) & ( $3 is Sub_negative implies $1 = F4(($2 . (Sub_the_argument_of $3))) ) & ( $3 is Sub_conjunctive implies $1 = F5(($2 . (Sub_the_left_argument_of $3)),($2 . (Sub_the_right_argument_of $3))) ) & ( $3 is Sub_universal implies $1 = F6($3,($2 . (Sub_the_scope_of $3))) ) );
defpred S2[ Function of QC-Sub-WFF ,F1(), Element of NAT ] means for S being Element of QC-Sub-WFF st len (@ (S `1 )) <= $2 holds
( ( S is Sub_VERUM implies $1 . S = F2() ) & ( S is Sub_atomic implies $1 . S = F3(S) ) & ( S is Sub_negative implies $1 . S = F4(($1 . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies $1 . S = F5(($1 . (Sub_the_left_argument_of S)),($1 . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies $1 . S = F6(S,($1 . (Sub_the_scope_of S))) ) );
defpred S3[ Element of NAT ] means ex F being Function of QC-Sub-WFF ,F1() st S2[F,$1];
A1: S3[ 0 ]
proof
consider F being Function of QC-Sub-WFF ,F1();
take F ; :: thesis: S2[F, 0 ]
let S be Element of QC-Sub-WFF ; :: thesis: ( len (@ (S `1 )) <= 0 implies ( ( S is Sub_VERUM implies F . S = F2() ) & ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative implies F . S = F4((F . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies F . S = F5((F . (Sub_the_left_argument_of S)),(F . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies F . S = F6(S,(F . (Sub_the_scope_of S))) ) ) )
assume A2: len (@ (S `1 )) <= 0 ; :: thesis: ( ( S is Sub_VERUM implies F . S = F2() ) & ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative implies F . S = F4((F . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies F . S = F5((F . (Sub_the_left_argument_of S)),(F . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies F . S = F6(S,(F . (Sub_the_scope_of S))) ) )
thus ( ( S is Sub_VERUM implies F . S = F2() ) & ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative implies F . S = F4((F . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies F . S = F5((F . (Sub_the_left_argument_of S)),(F . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies F . S = F6(S,(F . (Sub_the_scope_of S))) ) ) by A2, QC_LANG1:34; :: thesis: verum
end;
A3: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S3[n] implies S3[n + 1] )
given F being Function of QC-Sub-WFF ,F1() such that A4: S2[F,n] ; :: thesis: S3[n + 1]
defpred S4[ Element of QC-Sub-WFF , Element of F1()] means ( ( len (@ ($1 `1 )) <> n + 1 implies $2 = F . $1 ) & ( len (@ ($1 `1 )) = n + 1 implies S1[$2,F,$1] ) );
A5: for S being Element of QC-Sub-WFF ex y being Element of F1() st S4[S,y]
proof
let S be Element of QC-Sub-WFF ; :: thesis: ex y being Element of F1() st S4[S,y]
now
per cases ( len (@ (S `1 )) <> n + 1 or ( len (@ (S `1 )) = n + 1 & S is Sub_VERUM ) or ( len (@ (S `1 )) = n + 1 & S is Sub_atomic ) or ( len (@ (S `1 )) = n + 1 & S is Sub_negative ) or ( len (@ (S `1 )) = n + 1 & S is Sub_conjunctive ) or ( len (@ (S `1 )) = n + 1 & S is Sub_universal ) ) by Th12;
case len (@ (S `1 )) <> n + 1 ; :: thesis: ex y being Element of F1() st y = F . S
take y = F . S; :: thesis: y = F . S
thus y = F . S ; :: thesis: verum
end;
case A6: ( len (@ (S `1 )) = n + 1 & S is Sub_VERUM ) ; :: thesis: ex y being Element of F1() st S1[y,F,S]
take y = F2(); :: thesis: S1[y,F,S]
thus S1[y,F,S] by A6, Th27; :: thesis: verum
end;
case A7: ( len (@ (S `1 )) = n + 1 & S is Sub_atomic ) ; :: thesis: ex y being Element of F1() st S1[y,F,S]
take y = F3(S); :: thesis: S1[y,F,S]
thus S1[y,F,S] by A7, Th27; :: thesis: verum
end;
case A8: ( len (@ (S `1 )) = n + 1 & S is Sub_negative ) ; :: thesis: ex y being Element of F1() st S1[y,F,S]
take y = F4((F . (Sub_the_argument_of S))); :: thesis: S1[y,F,S]
thus S1[y,F,S] by A8, Th27; :: thesis: verum
end;
case A9: ( len (@ (S `1 )) = n + 1 & S is Sub_conjunctive ) ; :: thesis: ex y being Element of F1() st S1[y,F,S]
take y = F5((F . (Sub_the_left_argument_of S)),(F . (Sub_the_right_argument_of S))); :: thesis: S1[y,F,S]
thus S1[y,F,S] by A9, Th27; :: thesis: verum
end;
case A10: ( len (@ (S `1 )) = n + 1 & S is Sub_universal ) ; :: thesis: ex y being Element of F1() st S1[y,F,S]
take y = F6(S,(F . (Sub_the_scope_of S))); :: thesis: S1[y,F,S]
thus S1[y,F,S] by A10, Th27; :: thesis: verum
end;
end;
end;
hence ex y being Element of F1() st S4[S,y] ; :: thesis: verum
end;
consider G being Function of QC-Sub-WFF ,F1() such that
A11: for S being Element of QC-Sub-WFF holds S4[S,G . S] from FUNCT_2:sch 3(A5);
 take H = G; :: thesis: S2[H,n + 1]
thus S2[H,n + 1] :: thesis: verum
proof
let S be Element of QC-Sub-WFF ; :: thesis: ( len (@ (S `1 )) <= n + 1 implies ( ( S is Sub_VERUM implies H . S = F2() ) & ( S is Sub_atomic implies H . S = F3(S) ) & ( S is Sub_negative implies H . S = F4((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F6(S,(H . (Sub_the_scope_of S))) ) ) )
assume A12: len (@ (S `1 )) <= n + 1 ; :: thesis: ( ( S is Sub_VERUM implies H . S = F2() ) & ( S is Sub_atomic implies H . S = F3(S) ) & ( S is Sub_negative implies H . S = F4((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F6(S,(H . (Sub_the_scope_of S))) ) )
thus ( S is Sub_VERUM implies H . S = F2() ) :: thesis: ( ( S is Sub_atomic implies H . S = F3(S) ) & ( S is Sub_negative implies H . S = F4((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F6(S,(H . (Sub_the_scope_of S))) ) )
proof
now
per cases ( len (@ (S `1 )) <> n + 1 or len (@ (S `1 )) = n + 1 ) ;
suppose A13: len (@ (S `1 )) <> n + 1 ; :: thesis: ( S is Sub_VERUM implies H . S = F2() )
then A14: len (@ (S `1 )) <= n by A12, NAT_1:8;
H . S = F . S by A11, A13;
hence ( S is Sub_VERUM implies H . S = F2() ) by A4, A14; :: thesis: verum
end;
suppose len (@ (S `1 )) = n + 1 ; :: thesis: ( S is Sub_VERUM implies H . S = F2() )
hence ( S is Sub_VERUM implies H . S = F2() ) by A11; :: thesis: verum
end;
end;
end;
hence ( S is Sub_VERUM implies H . S = F2() ) ; :: thesis: verum
end;
thus ( S is Sub_atomic implies H . S = F3(S) ) :: thesis: ( ( S is Sub_negative implies H . S = F4((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F6(S,(H . (Sub_the_scope_of S))) ) )
proof
now
per cases ( len (@ (S `1 )) <> n + 1 or len (@ (S `1 )) = n + 1 ) ;
suppose A15: len (@ (S `1 )) <> n + 1 ; :: thesis: ( S is Sub_atomic implies H . S = F3(S) )
then A16: len (@ (S `1 )) <= n by A12, NAT_1:8;
H . S = F . S by A11, A15;
hence ( S is Sub_atomic implies H . S = F3(S) ) by A4, A16; :: thesis: verum
end;
suppose len (@ (S `1 )) = n + 1 ; :: thesis: ( S is Sub_atomic implies H . S = F3(S) )
hence ( S is Sub_atomic implies H . S = F3(S) ) by A11; :: thesis: verum
end;
end;
end;
hence ( S is Sub_atomic implies H . S = F3(S) ) ; :: thesis: verum
end;
thus ( S is Sub_negative implies H . S = F4((H . (Sub_the_argument_of S))) ) :: thesis: ( ( S is Sub_conjunctive implies H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F6(S,(H . (Sub_the_scope_of S))) ) )
proof
assume A17: S is Sub_negative ; :: thesis: H . S = F4((H . (Sub_the_argument_of S)))
then len (@ ((Sub_the_argument_of S) `1 )) <> n + 1 by A12, Th22;
then A18: H . (Sub_the_argument_of S) = F . (Sub_the_argument_of S) by A11;
now
per cases ( len (@ (S `1 )) <> n + 1 or len (@ (S `1 )) = n + 1 ) ;
suppose A19: len (@ (S `1 )) <> n + 1 ; :: thesis: H . S = F4((H . (Sub_the_argument_of S)))
then A20: len (@ (S `1 )) <= n by A12, NAT_1:8;
H . S = F . S by A11, A19;
hence H . S = F4((H . (Sub_the_argument_of S))) by A4, A17, A18, A20; :: thesis: verum
end;
suppose len (@ (S `1 )) = n + 1 ; :: thesis: H . S = F4((H . (Sub_the_argument_of S)))
hence H . S = F4((H . (Sub_the_argument_of S))) by A11, A17, A18; :: thesis: verum
end;
end;
end;
hence H . S = F4((H . (Sub_the_argument_of S))) ; :: thesis: verum
end;
thus ( S is Sub_conjunctive implies H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) :: thesis: ( S is Sub_universal implies H . S = F6(S,(H . (Sub_the_scope_of S))) )
proof
assume A21: S is Sub_conjunctive ; :: thesis: H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S)))
then len (@ ((Sub_the_left_argument_of S) `1 )) <> n + 1 by A12, Th23;
then A22: H . (Sub_the_left_argument_of S) = F . (Sub_the_left_argument_of S) by A11;
len (@ ((Sub_the_right_argument_of S) `1 )) <> n + 1 by A12, A21, Th23;
then A23: H . (Sub_the_right_argument_of S) = F . (Sub_the_right_argument_of S) by A11;
now
per cases ( len (@ (S `1 )) <> n + 1 or len (@ (S `1 )) = n + 1 ) ;
end;
end;
hence H . S = F5((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ; :: thesis: verum
end;
thus ( S is Sub_universal implies H . S = F6(S,(H . (Sub_the_scope_of S))) ) :: thesis: verum
proof
assume A26: S is Sub_universal ; :: thesis: H . S = F6(S,(H . (Sub_the_scope_of S)))
then len (@ ((Sub_the_scope_of S) `1 )) <> n + 1 by A12, Th24;
then A27: H . (Sub_the_scope_of S) = F . (Sub_the_scope_of S) by A11;
now
per cases ( len (@ (S `1 )) <> n + 1 or len (@ (S `1 )) = n + 1 ) ;
suppose A28: len (@ (S `1 )) <> n + 1 ; :: thesis: H . S = F6(S,(H . (Sub_the_scope_of S)))
then A29: len (@ (S `1 )) <= n by A12, NAT_1:8;
H . S = F . S by A11, A28;
hence H . S = F6(S,(H . (Sub_the_scope_of S))) by A4, A26, A27, A29; :: thesis: verum
end;
suppose len (@ (S `1 )) = n + 1 ; :: thesis: H . S = F6(S,(H . (Sub_the_scope_of S)))
hence H . S = F6(S,(H . (Sub_the_scope_of S))) by A11, A26, A27; :: thesis: verum
end;
end;
end;
hence H . S = F6(S,(H . (Sub_the_scope_of S))) ; :: thesis: verum
end;
end;
end;
A30: for n being Element of NAT holds S3[n] from NAT_1:sch 1(A1, A3);
 defpred S4[ set , set ] means ex S being Element of QC-Sub-WFF st
( S = $1 & ( for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (S `1 ))] holds
$2 = g . S ) );
A37: for x being set st x in QC-Sub-WFF holds
ex y being set st S4[x,y]
proof
let x be set ; :: thesis: ( x in QC-Sub-WFF implies ex y being set st S4[x,y] )
assume x in QC-Sub-WFF ; :: thesis: ex y being set st S4[x,y]
then reconsider x' = x as Element of QC-Sub-WFF ;
consider F being Function of QC-Sub-WFF ,F1() such that
A38: S2[F, len (@ (x' `1 ))] by A30;
take F . x ; :: thesis: S4[x,F . x]
take x' ; :: thesis: ( x' = x & ( for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (x' `1 ))] holds
F . x = g . x' ) )
thus x' = x ; :: thesis: for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (x' `1 ))] holds
F . x = g . x'
let G be Function of QC-Sub-WFF ,F1(); :: thesis: ( S2[G, len (@ (x' `1 ))] implies F . x = G . x' )
assume A39: S2[G, len (@ (x' `1 ))] ; :: thesis: F . x = G . x'
defpred S5[ Element of QC-Sub-WFF ] means ( len (@ ($1 `1 )) <= len (@ (x' `1 )) implies F . $1 = G . $1 );
A40: now
let S be Element of QC-Sub-WFF ; :: thesis: ( ( S is Sub_atomic implies S5[S] ) & ( S is Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
thus ( S is Sub_atomic implies S5[S] ) :: thesis: ( ( S is Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume that
A41: S is Sub_atomic and
A42: len (@ (S `1 )) <= len (@ (x' `1 )) ; :: thesis: F . S = G . S
thus F . S = F3(S) by A38, A41, A42
.= G . S by A39, A41, A42 ; :: thesis: verum
end;
thus ( S is Sub_VERUM implies S5[S] ) :: thesis: ( ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume that
A43: S is Sub_VERUM and
A44: len (@ (S `1 )) <= len (@ (x' `1 )) ; :: thesis: F . S = G . S
thus F . S = F2() by A38, A43, A44
.= G . S by A39, A43, A44 ; :: thesis: verum
end;
thus ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) :: thesis: ( ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume that
A45: S is Sub_negative and
A46: S5[ Sub_the_argument_of S] and
A47: len (@ (S `1 )) <= len (@ (x' `1 )) ; :: thesis: F . S = G . S
len (@ ((Sub_the_argument_of S) `1 )) < len (@ (S `1 )) by A45, Th22;
hence F . S = F4((G . (Sub_the_argument_of S))) by A38, A45, A46, A47, XXREAL_0:2
.= G . S by A39, A45, A47 ;
:: thesis: verum
end;
thus ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) :: thesis: ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] )thus ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) :: thesis: verum
proof
assume that
A53: S is Sub_universal and
A54: S5[ Sub_the_scope_of S] and
A55: len (@ (S `1 )) <= len (@ (x' `1 )) ; :: thesis: F . S = G . S
len (@ ((Sub_the_scope_of S) `1 )) < len (@ (S `1 )) by A53, Th24;
hence F . S = F6(S,(G . (Sub_the_scope_of S))) by A38, A53, A54, A55, XXREAL_0:2
.= G . S by A39, A53, A55 ;
:: thesis: verum
end;
end;
for S being Element of QC-Sub-WFF holds S5[S] from SUBSTUT1:sch 2(A40);
 hence F . x = G . x' ; :: thesis: verum
end;
consider F being Function such that
A56: dom F = QC-Sub-WFF and
A57: for x being set st x in QC-Sub-WFF holds
S4[x,F . x] from CLASSES1:sch 1(A37);
 rng F c= F1()
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in F1() )
assume y in rng F ; :: thesis: y in F1()
then consider x being set such that
A58: x in QC-Sub-WFF and
A59: y = F . x by A56, FUNCT_1:def 5;
consider S being Element of QC-Sub-WFF such that
S = x and
A60: for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (S `1 ))] holds
y = g . S by A57, A58, A59;
consider G being Function of QC-Sub-WFF ,F1() such that
A61: S2[G, len (@ (S `1 ))] by A30;
y = G . S by A60, A61;
hence y in F1() ; :: thesis: verum
end;
then reconsider F = F as Function of QC-Sub-WFF ,F1() by A56, FUNCT_2:def 1, RELSET_1:11;
take F ; :: thesis: for S being Element of QC-Sub-WFF
for d1, d2 being Element of F1() holds
( ( S is Sub_VERUM implies F . S = F2() ) & ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F4(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) ) )
let S be Element of QC-Sub-WFF ; :: thesis: for d1, d2 being Element of F1() holds
( ( S is Sub_VERUM implies F . S = F2() ) & ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F4(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) ) )
let d1, d2 be Element of F1(); :: thesis: ( ( S is Sub_VERUM implies F . S = F2() ) & ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F4(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) ) )
consider S1 being Element of QC-Sub-WFF such that
A62: S1 = S and
A63: for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (S1 `1 ))] holds
F . S = g . S1 by A57;
consider G being Function of QC-Sub-WFF ,F1() such that
A64: S2[G, len (@ (S1 `1 ))] by A30;
A65: F . S = G . S by A62, A63, A64;
hence ( S is Sub_VERUM implies F . S = F2() ) by A62, A64; :: thesis: ( ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F4(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) ) )
thus ( S is Sub_atomic implies F . S = F3(S) ) by A62, A64, A65; :: thesis: ( ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F4(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) ) )
A66: for k being Element of NAT st k < len (@ (S `1 )) holds
S2[G,k]
proof
let k be Element of NAT ; :: thesis: ( k < len (@ (S `1 )) implies S2[G,k] )
assume A67: k < len (@ (S `1 )) ; :: thesis: S2[G,k]
let S' be Element of QC-Sub-WFF ; :: thesis: ( len (@ (S' `1 )) <= k implies ( ( S' is Sub_VERUM implies G . S' = F2() ) & ( S' is Sub_atomic implies G . S' = F3(S') ) & ( S' is Sub_negative implies G . S' = F4((G . (Sub_the_argument_of S'))) ) & ( S' is Sub_conjunctive implies G . S' = F5((G . (Sub_the_left_argument_of S')),(G . (Sub_the_right_argument_of S'))) ) & ( S' is Sub_universal implies G . S' = F6(S',(G . (Sub_the_scope_of S'))) ) ) )
assume len (@ (S' `1 )) <= k ; :: thesis: ( ( S' is Sub_VERUM implies G . S' = F2() ) & ( S' is Sub_atomic implies G . S' = F3(S') ) & ( S' is Sub_negative implies G . S' = F4((G . (Sub_the_argument_of S'))) ) & ( S' is Sub_conjunctive implies G . S' = F5((G . (Sub_the_left_argument_of S')),(G . (Sub_the_right_argument_of S'))) ) & ( S' is Sub_universal implies G . S' = F6(S',(G . (Sub_the_scope_of S'))) ) )
then len (@ (S' `1 )) <= len (@ (S `1 )) by A67, XXREAL_0:2;
hence ( ( S' is Sub_VERUM implies G . S' = F2() ) & ( S' is Sub_atomic implies G . S' = F3(S') ) & ( S' is Sub_negative implies G . S' = F4((G . (Sub_the_argument_of S'))) ) & ( S' is Sub_conjunctive implies G . S' = F5((G . (Sub_the_left_argument_of S')),(G . (Sub_the_right_argument_of S'))) ) & ( S' is Sub_universal implies G . S' = F6(S',(G . (Sub_the_scope_of S'))) ) ) by A62, A64; :: thesis: verum
end;
thus ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F4(d1) ) :: thesis: ( ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) ) )
proof
assume A68: S is Sub_negative ; :: thesis: ( not d1 = F . (Sub_the_argument_of S) or F . S = F4(d1) )
set S' = Sub_the_argument_of S;
set k = len (@ ((Sub_the_argument_of S) `1 ));
len (@ ((Sub_the_argument_of S) `1 )) < len (@ (S `1 )) by A68, Th22;
then A69: S2[G, len (@ ((Sub_the_argument_of S) `1 ))] by A66;
ex S1 being Element of QC-Sub-WFF st
( S1 = Sub_the_argument_of S & ( for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (S1 `1 ))] holds
F . (Sub_the_argument_of S) = g . S1 ) ) by A57;
then F . (Sub_the_argument_of S) = G . (Sub_the_argument_of S) by A69;
hence ( not d1 = F . (Sub_the_argument_of S) or F . S = F4(d1) ) by A62, A64, A65, A68; :: thesis: verum
end;
thus ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) :: thesis: ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) )
proof
assume A70: S is Sub_conjunctive ; :: thesis: ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F5(d1,d2) )
set S' = Sub_the_left_argument_of S;
set k' = len (@ ((Sub_the_left_argument_of S) `1 ));
set S'' = Sub_the_right_argument_of S;
set k'' = len (@ ((Sub_the_right_argument_of S) `1 ));
len (@ ((Sub_the_left_argument_of S) `1 )) < len (@ (S `1 )) by A70, Th23;
then A71: S2[G, len (@ ((Sub_the_left_argument_of S) `1 ))] by A66;
len (@ ((Sub_the_right_argument_of S) `1 )) < len (@ (S `1 )) by A70, Th23;
then A72: S2[G, len (@ ((Sub_the_right_argument_of S) `1 ))] by A66;
A73: ex S1 being Element of QC-Sub-WFF st
( S1 = Sub_the_left_argument_of S & ( for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (S1 `1 ))] holds
F . (Sub_the_left_argument_of S) = g . S1 ) ) by A57;
A74: ex S2 being Element of QC-Sub-WFF st
( S2 = Sub_the_right_argument_of S & ( for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (S2 `1 ))] holds
F . (Sub_the_right_argument_of S) = g . S2 ) ) by A57;
A75: F . (Sub_the_left_argument_of S) = G . (Sub_the_left_argument_of S) by A71, A73;
F . (Sub_the_right_argument_of S) = G . (Sub_the_right_argument_of S) by A72, A74;
hence ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F5(d1,d2) ) by A62, A64, A65, A70, A75; :: thesis: verum
end;
assume A76: S is Sub_universal ; :: thesis: ( not d1 = F . (Sub_the_scope_of S) or F . S = F6(S,d1) )
set S' = Sub_the_scope_of S;
set k = len (@ ((Sub_the_scope_of S) `1 ));
len (@ ((Sub_the_scope_of S) `1 )) < len (@ (S `1 )) by A76, Th24;
then A77: S2[G, len (@ ((Sub_the_scope_of S) `1 ))] by A66;
ex S1 being Element of QC-Sub-WFF st
( S1 = Sub_the_scope_of S & ( for g being Function of QC-Sub-WFF ,F1() st S2[g, len (@ (S1 `1 ))] holds
F . (Sub_the_scope_of S) = g . S1 ) ) by A57;
then F . (Sub_the_scope_of S) = G . (Sub_the_scope_of S) by A77;
hence ( not d1 = F . (Sub_the_scope_of S) or F . S = F6(S,d1) ) by A62, A64, A65, A76; :: thesis: verum