defpred S1[ Function of (QC-WFF F1()),F2(), Nat] means ( $1 . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() st len (@ p) <= $2 holds
( ( p is atomic implies $1 . p = F4(p) ) & ( p is negative implies $1 . p = F5(($1 . (the_argument_of p))) ) & ( p is conjunctive implies $1 . p = F6(($1 . (the_left_argument_of p)),($1 . (the_right_argument_of p))) ) & ( p is universal implies $1 . p = F7(p,($1 . (the_scope_of p))) ) ) ) );
defpred S2[ Element of F2(), Function of (QC-WFF F1()),F2(), Element of QC-WFF F1()] means ( ( $3 = VERUM F1() implies $1 = F3() ) & ( $3 is atomic implies $1 = F4($3) ) & ( $3 is negative implies $1 = F5(($2 . (the_argument_of $3))) ) & ( $3 is conjunctive implies $1 = F6(($2 . (the_left_argument_of $3)),($2 . (the_right_argument_of $3))) ) & ( $3 is universal implies $1 = F7($3,($2 . (the_scope_of $3))) ) );
defpred S3[ Nat] means ex F being Function of (QC-WFF F1()),F2() st S1[F,$1];
defpred S4[ object , object ] means ex p being Element of QC-WFF F1() st
( p = $1 & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p)] holds
$2 = g . p ) );
A1: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
given F being Function of (QC-WFF F1()),F2() such that A2: S1[F,n] ; :: thesis: S3[n + 1]
defpred S5[ Element of QC-WFF F1(), Element of F2()] means ( ( len (@ $1) <> n + 1 implies $2 = F . $1 ) & ( len (@ $1) = n + 1 implies S2[$2,F,$1] ) );
A3: for p being Element of QC-WFF F1() ex y being Element of F2() st S5[p,y]
proof
let p be Element of QC-WFF F1(); :: thesis: ex y being Element of F2() st S5[p,y]
now :: thesis: ( ( len (@ p) <> n + 1 & ex y being Element of F2() st y = F . p ) or ( len (@ p) = n + 1 & p = VERUM F1() & ex y being Element of F2() st S2[y,F,p] ) or ( len (@ p) = n + 1 & p is atomic & ex y being Element of F2() st S2[y,F,p] ) or ( len (@ p) = n + 1 & p is negative & ex y being Element of F2() st S2[y,F,p] ) or ( len (@ p) = n + 1 & p is conjunctive & ex y being Element of F2() st S2[y,F,p] ) or ( len (@ p) = n + 1 & p is universal & ex y being Element of F2() st S2[y,F,p] ) )
per cases ( len (@ p) <> n + 1 or ( len (@ p) = n + 1 & p = VERUM F1() ) or ( len (@ p) = n + 1 & p is atomic ) or ( len (@ p) = n + 1 & p is negative ) or ( len (@ p) = n + 1 & p is conjunctive ) or ( len (@ p) = n + 1 & p is universal ) ) by Th9;
case len (@ p) <> n + 1 ; :: thesis: ex y being Element of F2() st y = F . p
take y = F . p; :: thesis: y = F . p
thus y = F . p ; :: thesis: verum
end;
case A4: ( len (@ p) = n + 1 & p = VERUM F1() ) ; :: thesis: ex y being Element of F2() st S2[y,F,p]
take y = F3(); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A4, Th20; :: thesis: verum
end;
case A5: ( len (@ p) = n + 1 & p is atomic ) ; :: thesis: ex y being Element of F2() st S2[y,F,p]
take y = F4(p); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A5, Th20; :: thesis: verum
end;
case A6: ( len (@ p) = n + 1 & p is negative ) ; :: thesis: ex y being Element of F2() st S2[y,F,p]
take y = F5((F . (the_argument_of p))); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A6, Th20; :: thesis: verum
end;
case A7: ( len (@ p) = n + 1 & p is conjunctive ) ; :: thesis: ex y being Element of F2() st S2[y,F,p]
take y = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A7, Th20; :: thesis: verum
end;
case A8: ( len (@ p) = n + 1 & p is universal ) ; :: thesis: ex y being Element of F2() st S2[y,F,p]
take y = F7(p,(F . (the_scope_of p))); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A8, Th20; :: thesis: verum
end;
end;
end;
hence ex y being Element of F2() st S5[p,y] ; :: thesis: verum
end;
consider G being Function of (QC-WFF F1()),F2() such that
A9: for p being Element of QC-WFF F1() holds S5[p,G . p] from FUNCT_2:sch 3(A3);
 take H = G; :: thesis: S1[H,n + 1]
thus S1[H,n + 1] :: thesis: verum
proof
thus H . (VERUM F1()) = F3() :: thesis: for p being Element of QC-WFF F1() st len (@ p) <= n + 1 holds
( ( p is atomic implies H . p = F4(p) ) & ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
proof
per cases ( len (@ (VERUM F1())) <> n + 1 or len (@ (VERUM F1())) = n + 1 ) ;
suppose len (@ (VERUM F1())) <> n + 1 ; :: thesis: H . (VERUM F1()) = F3()
hence H . (VERUM F1()) = F3() by A2, A9; :: thesis: verum
end;
suppose len (@ (VERUM F1())) = n + 1 ; :: thesis: H . (VERUM F1()) = F3()
hence H . (VERUM F1()) = F3() by A9; :: thesis: verum
end;
end;
end;
let p be Element of QC-WFF F1(); :: thesis: ( len (@ p) <= n + 1 implies ( ( p is atomic implies H . p = F4(p) ) & ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) ) )
assume A10: len (@ p) <= n + 1 ; :: thesis: ( ( p is atomic implies H . p = F4(p) ) & ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
thus ( p is atomic implies H . p = F4(p) ) :: thesis: ( ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
proof
now :: thesis: ( p is atomic implies H . p = F4(p) )
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; :: thesis: ( p is atomic implies H . p = F4(p) )
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence ( p is atomic implies H . p = F4(p) ) by A2; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: ( p is atomic implies H . p = F4(p) )
hence ( p is atomic implies H . p = F4(p) ) by A9; :: thesis: verum
end;
end;
end;
hence ( p is atomic implies H . p = F4(p) ) ; :: thesis: verum
end;
thus ( p is negative implies H . p = F5((H . (the_argument_of p))) ) :: thesis: ( ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
proof
assume A11: p is negative ; :: thesis: H . p = F5((H . (the_argument_of p)))
then len (@ (the_argument_of p)) <> n + 1 by A10, Th14;
then A12: H . (the_argument_of p) = F . (the_argument_of p) by A9;
now :: thesis: H . p = F5((H . (the_argument_of p)))
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; :: thesis: H . p = F5((H . (the_argument_of p)))
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence H . p = F5((H . (the_argument_of p))) by A2, A11, A12; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: H . p = F5((H . (the_argument_of p)))
hence H . p = F5((H . (the_argument_of p))) by A9, A11, A12; :: thesis: verum
end;
end;
end;
hence H . p = F5((H . (the_argument_of p))) ; :: thesis: verum
end;
thus ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) :: thesis: ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) )
proof
assume A13: p is conjunctive ; :: thesis: H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p)))
then len (@ (the_right_argument_of p)) <> n + 1 by A10, Th15;
then A14: H . (the_right_argument_of p) = F . (the_right_argument_of p) by A9;
len (@ (the_left_argument_of p)) <> n + 1 by A10, A13, Th15;
then A15: H . (the_left_argument_of p) = F . (the_left_argument_of p) by A9;
now :: thesis: H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p)))
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; :: thesis: H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p)))
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) by A2, A13, A15, A14; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p)))
hence H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) by A9, A13, A15, A14; :: thesis: verum
end;
end;
end;
hence H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ; :: thesis: verum
end;
thus ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) :: thesis: verum
proof
assume A16: p is universal ; :: thesis: H . p = F7(p,(H . (the_scope_of p)))
then len (@ (the_scope_of p)) <> n + 1 by A10, Th16;
then A17: H . (the_scope_of p) = F . (the_scope_of p) by A9;
now :: thesis: H . p = F7(p,(H . (the_scope_of p)))
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; :: thesis: H . p = F7(p,(H . (the_scope_of p)))
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence H . p = F7(p,(H . (the_scope_of p))) by A2, A16, A17; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: H . p = F7(p,(H . (the_scope_of p)))
hence H . p = F7(p,(H . (the_scope_of p))) by A9, A16, A17; :: thesis: verum
end;
end;
end;
hence H . p = F7(p,(H . (the_scope_of p))) ; :: thesis: verum
end;
end;
end;
A18: S3[ 0 ]
proof
reconsider F = (QC-WFF F1()) --> F3() as Function of (QC-WFF F1()),F2() ;
take F ; :: thesis: S1[F, 0 ]
thus F . (VERUM F1()) = F3() by FUNCOP_1:7; :: thesis: for p being Element of QC-WFF F1() st len (@ p) <= 0 holds
( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
let p be Element of QC-WFF F1(); :: thesis: ( len (@ p) <= 0 implies ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) )
assume A19: len (@ p) <= 0 ; :: thesis: ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
1 <= len (@ p) by Th10;
hence ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) by A19; :: thesis: verum
end;
A20: for n being Nat holds S3[n] from NAT_1:sch 2(A18, A1);
 then A21: ex G being Function of (QC-WFF F1()),F2() st S1[G, len (@ (VERUM F1()))] ;
A22: for x being object st x in QC-WFF F1() holds
ex y being object st S4[x,y]
proof
let x be object ; :: thesis: ( x in QC-WFF F1() implies ex y being object st S4[x,y] )
assume x in QC-WFF F1() ; :: thesis: ex y being object st S4[x,y]
then reconsider x9 = x as Element of QC-WFF F1() ;
consider F being Function of (QC-WFF F1()),F2() such that
A23: S1[F, len (@ x9)] by A20;
take F . x ; :: thesis: S4[x,F . x]
take x9 ; :: thesis: ( x9 = x & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ x9)] holds
F . x = g . x9 ) )
thus x = x9 ; :: thesis: for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ x9)] holds
F . x = g . x9
let G be Function of (QC-WFF F1()),F2(); :: thesis: ( S1[G, len (@ x9)] implies F . x = G . x9 )
assume A24: S1[G, len (@ x9)] ; :: thesis: F . x = G . x9
defpred S5[ Element of QC-WFF F1()] means ( len (@ $1) <= len (@ x9) implies F . $1 = G . $1 );
A25: now :: thesis: for p being Element of QC-WFF F1() holds
( ( p is atomic implies S5[p] ) & S5[ VERUM F1()] & ( p is negative & S5[ the_argument_of p] implies S5[p] ) & ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
let p be Element of QC-WFF F1(); :: thesis: ( ( p is atomic implies S5[p] ) & S5[ VERUM F1()] & ( p is negative & S5[ the_argument_of p] implies S5[p] ) & ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
thus ( p is atomic implies S5[p] ) :: thesis: ( S5[ VERUM F1()] & ( p is negative & S5[ the_argument_of p] implies S5[p] ) & ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
proof
assume A26: ( p is atomic & len (@ p) <= len (@ x9) ) ; :: thesis: F . p = G . p
hence F . p = F4(p) by A23
.= G . p by A24, A26 ;
:: thesis: verum
end;
thus S5[ VERUM F1()] by A23, A24; :: thesis: ( ( p is negative & S5[ the_argument_of p] implies S5[p] ) & ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
thus ( p is negative & S5[ the_argument_of p] implies S5[p] ) :: thesis: ( ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
proof
assume that
A27: p is negative and
A28: S5[ the_argument_of p] and
A29: len (@ p) <= len (@ x9) ; :: thesis: F . p = G . p
len (@ (the_argument_of p)) < len (@ p) by A27, Th14;
hence F . p = F5((G . (the_argument_of p))) by A23, A27, A28, A29, XXREAL_0:2
.= G . p by A24, A27, A29 ;
:: thesis: verum
end;
thus ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) :: thesis: ( p is universal & S5[ the_scope_of p] implies S5[p] )
proof
assume that
A30: p is conjunctive and
A31: ( S5[ the_left_argument_of p] & S5[ the_right_argument_of p] ) and
A32: len (@ p) <= len (@ x9) ; :: thesis: F . p = G . p
( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) ) by A30, Th15;
hence F . p = F6((G . (the_left_argument_of p)),(G . (the_right_argument_of p))) by A23, A30, A31, A32, XXREAL_0:2
.= G . p by A24, A30, A32 ;
:: thesis: verum
end;
thus ( p is universal & S5[ the_scope_of p] implies S5[p] ) :: thesis: verum
proof
assume that
A33: p is universal and
A34: S5[ the_scope_of p] and
A35: len (@ p) <= len (@ x9) ; :: thesis: F . p = G . p
len (@ (the_scope_of p)) < len (@ p) by A33, Th16;
hence F . p = F7(p,(G . (the_scope_of p))) by A23, A33, A34, A35, XXREAL_0:2
.= G . p by A24, A33, A35 ;
:: thesis: verum
end;
end;
for p being Element of QC-WFF F1() holds S5[p] from QC_LANG1:sch 2(A25);
 hence F . x = G . x9 ; :: thesis: verum
end;
consider F being Function such that
A36: dom F = QC-WFF F1() and
A37: for x being object st x in QC-WFF F1() holds
S4[x,F . x] from CLASSES1:sch 1(A22);
 rng F c= F2()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in F2() )
assume y in rng F ; :: thesis: y in F2()
then consider x being object such that
A38: ( x in QC-WFF F1() & y = F . x ) by A36, FUNCT_1:def 3;
consider p being Element of QC-WFF F1() such that
p = x and
A39: for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p)] holds
y = g . p by A37, A38;
consider G being Function of (QC-WFF F1()),F2() such that
A40: S1[G, len (@ p)] by A20;
y = G . p by A39, A40;
hence y in F2() ; :: thesis: verum
end;
then reconsider F = F as Function of (QC-WFF F1()),F2() by A36, FUNCT_2:def 1, RELSET_1:4;
take F ; :: thesis: ( F . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) ) )
S4[ VERUM F1(),F . (VERUM F1())] by A37;
hence F . (VERUM F1()) = F3() by A21; :: thesis: for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
let p be Element of QC-WFF F1(); :: thesis: ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
consider p1 being Element of QC-WFF F1() such that
A41: p1 = p and
A42: for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . p = g . p1 by A37;
consider G being Function of (QC-WFF F1()),F2() such that
A43: S1[G, len (@ p1)] by A20;
set p9 = the_scope_of p;
A44: ex p1 being Element of QC-WFF F1() st
( p1 = the_scope_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . (the_scope_of p) = g . p1 ) ) by A37;
A45: F . p = G . p by A41, A42, A43;
hence ( p is atomic implies F . p = F4(p) ) by A41, A43; :: thesis: ( ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
A46: for k being Nat st k < len (@ p) holds
S1[G,k]
proof
let k be Nat; :: thesis: ( k < len (@ p) implies S1[G,k] )
assume A47: k < len (@ p) ; :: thesis: S1[G,k]
thus G . (VERUM F1()) = F3() by A43; :: thesis: for p being Element of QC-WFF F1() st len (@ p) <= k holds
( ( p is atomic implies G . p = F4(p) ) & ( p is negative implies G . p = F5((G . (the_argument_of p))) ) & ( p is conjunctive implies G . p = F6((G . (the_left_argument_of p)),(G . (the_right_argument_of p))) ) & ( p is universal implies G . p = F7(p,(G . (the_scope_of p))) ) )
let p9 be Element of QC-WFF F1(); :: thesis: ( len (@ p9) <= k implies ( ( p9 is atomic implies G . p9 = F4(p9) ) & ( p9 is negative implies G . p9 = F5((G . (the_argument_of p9))) ) & ( p9 is conjunctive implies G . p9 = F6((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9))) ) & ( p9 is universal implies G . p9 = F7(p9,(G . (the_scope_of p9))) ) ) )
assume len (@ p9) <= k ; :: thesis: ( ( p9 is atomic implies G . p9 = F4(p9) ) & ( p9 is negative implies G . p9 = F5((G . (the_argument_of p9))) ) & ( p9 is conjunctive implies G . p9 = F6((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9))) ) & ( p9 is universal implies G . p9 = F7(p9,(G . (the_scope_of p9))) ) )
then len (@ p9) <= len (@ p) by A47, XXREAL_0:2;
hence ( ( p9 is atomic implies G . p9 = F4(p9) ) & ( p9 is negative implies G . p9 = F5((G . (the_argument_of p9))) ) & ( p9 is conjunctive implies G . p9 = F6((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9))) ) & ( p9 is universal implies G . p9 = F7(p9,(G . (the_scope_of p9))) ) ) by A41, A43; :: thesis: verum
end;
thus ( p is negative implies F . p = F5((F . (the_argument_of p))) ) :: thesis: ( ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
proof
set p9 = the_argument_of p;
set k = len (@ (the_argument_of p));
A48: ex p1 being Element of QC-WFF F1() st
( p1 = the_argument_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . (the_argument_of p) = g . p1 ) ) by A37;
assume A49: p is negative ; :: thesis: F . p = F5((F . (the_argument_of p)))
then len (@ (the_argument_of p)) < len (@ p) by Th14;
then S1[G, len (@ (the_argument_of p))] by A46;
then F . (the_argument_of p) = G . (the_argument_of p) by A48;
hence F . p = F5((F . (the_argument_of p))) by A41, A43, A45, A49; :: thesis: verum
end;
thus ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) :: thesis: ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) )
proof
set p99 = the_right_argument_of p;
set p9 = the_left_argument_of p;
set k9 = len (@ (the_left_argument_of p));
set k99 = len (@ (the_right_argument_of p));
A50: ex p2 being Element of QC-WFF F1() st
( p2 = the_right_argument_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p2)] holds
F . (the_right_argument_of p) = g . p2 ) ) by A37;
assume A51: p is conjunctive ; :: thesis: F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p)))
then len (@ (the_left_argument_of p)) < len (@ p) by Th15;
then A52: S1[G, len (@ (the_left_argument_of p))] by A46;
len (@ (the_right_argument_of p)) < len (@ p) by A51, Th15;
then S1[G, len (@ (the_right_argument_of p))] by A46;
then A53: F . (the_right_argument_of p) = G . (the_right_argument_of p) by A50;
ex p1 being Element of QC-WFF F1() st
( p1 = the_left_argument_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . (the_left_argument_of p) = g . p1 ) ) by A37;
then F . (the_left_argument_of p) = G . (the_left_argument_of p) by A52;
hence F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) by A41, A43, A45, A51, A53; :: thesis: verum
end;
set k = len (@ (the_scope_of p));
assume A54: p is universal ; :: thesis: F . p = F7(p,(F . (the_scope_of p)))
then len (@ (the_scope_of p)) < len (@ p) by Th16;
then S1[G, len (@ (the_scope_of p))] by A46;
then F . (the_scope_of p) = G . (the_scope_of p) by A44;
hence F . p = F7(p,(F . (the_scope_of p))) by A41, A43, A45, A54; :: thesis: verum