defpred S1[ Function of QC-WFF,F1(), Nat] means for p being Element of QC-WFF st len (@ p) <= $2 holds
( ( p = VERUM implies $1 . p = F2() ) & ( p is atomic implies $1 . p = F3(p) ) & ( p is negative implies $1 . p = F4(($1 . (the_argument_of p)),p) ) & ( p is conjunctive implies $1 . p = F5(($1 . (the_left_argument_of p)),($1 . (the_right_argument_of p)),p) ) & ( p is universal implies $1 . p = F6(($1 . (the_scope_of p)),p) ) );
defpred S2[ Element of F1(), Function of QC-WFF,F1(), Element of QC-WFF ] means ( ( $3 = VERUM implies $1 = F2() ) & ( $3 is atomic implies $1 = F3($3) ) & ( $3 is negative implies $1 = F4(($2 . (the_argument_of $3)),$3) ) & ( $3 is conjunctive implies $1 = F5(($2 . (the_left_argument_of $3)),($2 . (the_right_argument_of $3)),$3) ) & ( $3 is universal implies $1 = F6(($2 . (the_scope_of $3)),$3) ) );
defpred S3[ Element of NAT ] means ex F being Function of QC-WFF,F1() st S1[F,$1];
A1: 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-WFF,F1() such that A2: S1[F,n] ; :: thesis: S3[n + 1]
defpred S4[ Element of QC-WFF , Element of F1()] means ( ( len (@ $1) <> n + 1 implies $2 = F . $1 ) & ( len (@ $1) = n + 1 implies S2[$2,F,$1] ) );
A3: for x being Element of QC-WFF ex y being Element of F1() st S4[x,y]
proof
let p be Element of QC-WFF ; :: thesis: ex y being Element of F1() st S4[p,y]
now
per cases ( len (@ p) <> n + 1 or ( len (@ p) = n + 1 & p = VERUM ) 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 QC_LANG1:7;
case len (@ p) <> n + 1 ; :: thesis: ex y being Element of F1() 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 ) ; :: thesis: ex y being Element of F1() st S2[y,F,p]
take y = F2(); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A4, QC_LANG1:18; :: thesis: verum
end;
case A5: ( len (@ p) = n + 1 & p is atomic ) ; :: thesis: ex y being Element of F1() st S2[y,F,p]
take y = F3(p); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A5, QC_LANG1:18; :: thesis: verum
end;
case A6: ( len (@ p) = n + 1 & p is negative ) ; :: thesis: ex y being Element of F1() st S2[y,F,p]
take y = F4((F . (the_argument_of p)),p); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A6, QC_LANG1:18; :: thesis: verum
end;
case A7: ( len (@ p) = n + 1 & p is conjunctive ) ; :: thesis: ex y being Element of F1() st S2[y,F,p]
take y = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A7, QC_LANG1:18; :: thesis: verum
end;
case A8: ( len (@ p) = n + 1 & p is universal ) ; :: thesis: ex y being Element of F1() st S2[y,F,p]
take y = F6((F . (the_scope_of p)),p); :: thesis: S2[y,F,p]
thus S2[y,F,p] by A8, QC_LANG1:18; :: thesis: verum
end;
end;
end;
hence ex y being Element of F1() st S4[p,y] ; :: thesis: verum
end;
consider G being Function of QC-WFF,F1() such that
A9: for p being Element of QC-WFF holds S4[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
let p be Element of QC-WFF ; :: thesis: ( len (@ p) <= n + 1 implies ( ( p = VERUM implies H . p = F2() ) & ( p is atomic implies H . p = F3(p) ) & ( p is negative implies H . p = F4((H . (the_argument_of p)),p) ) & ( p is conjunctive implies H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) ) & ( p is universal implies H . p = F6((H . (the_scope_of p)),p) ) ) )
assume A10: len (@ p) <= n + 1 ; :: thesis: ( ( p = VERUM implies H . p = F2() ) & ( p is atomic implies H . p = F3(p) ) & ( p is negative implies H . p = F4((H . (the_argument_of p)),p) ) & ( p is conjunctive implies H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) ) & ( p is universal implies H . p = F6((H . (the_scope_of p)),p) ) )
thus ( p = VERUM implies H . p = F2() ) :: thesis: ( ( p is atomic implies H . p = F3(p) ) & ( p is negative implies H . p = F4((H . (the_argument_of p)),p) ) & ( p is conjunctive implies H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) ) & ( p is universal implies H . p = F6((H . (the_scope_of p)),p) ) )
proof
now
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose A11: len (@ p) <> n + 1 ; :: thesis: ( p = VERUM implies H . p = F2() )
then A12: H . p = F . p by A9;
len (@ p) <= n by A10, A11, NAT_1:8;
hence ( p = VERUM implies H . p = F2() ) by A2, A12; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: ( p = VERUM implies H . p = F2() )
hence ( p = VERUM implies H . p = F2() ) by A9; :: thesis: verum
end;
end;
end;
hence ( p = VERUM implies H . p = F2() ) ; :: thesis: verum
end;
thus ( p is atomic implies H . p = F3(p) ) :: thesis: ( ( p is negative implies H . p = F4((H . (the_argument_of p)),p) ) & ( p is conjunctive implies H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) ) & ( p is universal implies H . p = F6((H . (the_scope_of p)),p) ) )
proof
now
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose A13: len (@ p) <> n + 1 ; :: thesis: ( p is atomic implies H . p = F3(p) )
then A14: H . p = F . p by A9;
len (@ p) <= n by A10, A13, NAT_1:8;
hence ( p is atomic implies H . p = F3(p) ) by A2, A14; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: ( p is atomic implies H . p = F3(p) )
hence ( p is atomic implies H . p = F3(p) ) by A9; :: thesis: verum
end;
end;
end;
hence ( p is atomic implies H . p = F3(p) ) ; :: thesis: verum
end;
thus ( p is negative implies H . p = F4((H . (the_argument_of p)),p) ) :: thesis: ( ( p is conjunctive implies H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) ) & ( p is universal implies H . p = F6((H . (the_scope_of p)),p) ) )
proof
assume A15: p is negative ; :: thesis: H . p = F4((H . (the_argument_of p)),p)
then len (@ (the_argument_of p)) <> n + 1 by A10, QC_LANG1:12;
then A16: H . (the_argument_of p) = F . (the_argument_of p) by A9;
now
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose A17: len (@ p) <> n + 1 ; :: thesis: H . p = F4((H . (the_argument_of p)),p)
then A18: H . p = F . p by A9;
len (@ p) <= n by A10, A17, NAT_1:8;
hence H . p = F4((H . (the_argument_of p)),p) by A2, A15, A16, A18; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: H . p = F4((H . (the_argument_of p)),p)
hence H . p = F4((H . (the_argument_of p)),p) by A9, A15, A16; :: thesis: verum
end;
end;
end;
hence H . p = F4((H . (the_argument_of p)),p) ; :: thesis: verum
end;
thus ( p is conjunctive implies H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) ) :: thesis: ( p is universal implies H . p = F6((H . (the_scope_of p)),p) )
proof
assume A19: p is conjunctive ; :: thesis: H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p)
then len (@ (the_right_argument_of p)) <> n + 1 by A10, QC_LANG1:13;
then A20: H . (the_right_argument_of p) = F . (the_right_argument_of p) by A9;
len (@ (the_left_argument_of p)) <> n + 1 by A10, A19, QC_LANG1:13;
then A21: H . (the_left_argument_of p) = F . (the_left_argument_of p) by A9;
now
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose A22: len (@ p) <> n + 1 ; :: thesis: H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p)
then A23: H . p = F . p by A9;
len (@ p) <= n by A10, A22, NAT_1:8;
hence H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) by A2, A19, A21, A20, A23; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p)
hence H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) by A9, A19, A21, A20; :: thesis: verum
end;
end;
end;
hence H . p = F5((H . (the_left_argument_of p)),(H . (the_right_argument_of p)),p) ; :: thesis: verum
end;
thus ( p is universal implies H . p = F6((H . (the_scope_of p)),p) ) :: thesis: verum
proof
assume A24: p is universal ; :: thesis: H . p = F6((H . (the_scope_of p)),p)
then len (@ (the_scope_of p)) <> n + 1 by A10, QC_LANG1:14;
then A25: H . (the_scope_of p) = F . (the_scope_of p) by A9;
now
per cases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose A26: len (@ p) <> n + 1 ; :: thesis: H . p = F6((H . (the_scope_of p)),p)
then A27: H . p = F . p by A9;
len (@ p) <= n by A10, A26, NAT_1:8;
hence H . p = F6((H . (the_scope_of p)),p) by A2, A24, A25, A27; :: thesis: verum
end;
suppose len (@ p) = n + 1 ; :: thesis: H . p = F6((H . (the_scope_of p)),p)
hence H . p = F6((H . (the_scope_of p)),p) by A9, A24, A25; :: thesis: verum
end;
end;
end;
hence H . p = F6((H . (the_scope_of p)),p) ; :: thesis: verum
end;
end;
end;
defpred S4[ set , set ] means ex p being Element of QC-WFF st
( p = $1 & ( for g being Function of QC-WFF,F1() st S1[g, len (@ p)] holds
$2 = g . p ) );
A28: S3[ 0 ]
proof
set F = the Function of QC-WFF,F1();
take the Function of QC-WFF,F1() ; :: thesis: S1[ the Function of QC-WFF,F1(), 0 ]
thus S1[ the Function of QC-WFF,F1(), 0 ] by QC_LANG1:8; :: thesis: verum
end;
A29: for n being Element of NAT holds S3[n] from NAT_1:sch 1(A28, A1);
 A30: for x being set st x in QC-WFF holds
ex y being set st S4[x,y]
proof
let x be set ; :: thesis: ( x in QC-WFF implies ex y being set st S4[x,y] )
assume x in QC-WFF ; :: thesis: ex y being set st S4[x,y]
then reconsider x9 = x as Element of QC-WFF ;
consider F being Function of QC-WFF,F1() such that
A31: S1[F, len (@ x9)] by A29;
take F . x ; :: thesis: S4[x,F . x]
take x9 ; :: thesis: ( x9 = x & ( for g being Function of QC-WFF,F1() st S1[g, len (@ x9)] holds
F . x = g . x9 ) )
thus x = x9 ; :: thesis: for g being Function of QC-WFF,F1() st S1[g, len (@ x9)] holds
F . x = g . x9
let G be Function of QC-WFF,F1(); :: thesis: ( S1[G, len (@ x9)] implies F . x = G . x9 )
assume A32: S1[G, len (@ x9)] ; :: thesis: F . x = G . x9
defpred S5[ Element of QC-WFF ] means ( len (@ $1) <= len (@ x9) implies F . $1 = G . $1 );
A33: now
let p be Element of QC-WFF ; :: thesis: ( ( p is atomic implies S5[p] ) & S5[ VERUM ] & ( 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 ] & ( 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 that
A34: p is atomic and
A35: len (@ p) <= len (@ x9) ; :: thesis: F . p = G . p
thus F . p = F3(p) by A31, A34, A35
.= G . p by A32, A34, A35 ; :: thesis: verum
end;
thus S5[ VERUM ] :: 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] ) )
proof
assume A36: len (@ VERUM) <= len (@ x9) ; :: thesis: F . VERUM = G . VERUM
hence F . VERUM = F2() by A31
.= G . VERUM by A32, A36 ;
:: thesis: verum
end;
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
A37: p is negative and
A38: S5[ the_argument_of p] and
A39: len (@ p) <= len (@ x9) ; :: thesis: F . p = G . p
len (@ (the_argument_of p)) < len (@ p) by A37, QC_LANG1:12;
hence F . p = F4((G . (the_argument_of p)),p) by A31, A37, A38, A39, XXREAL_0:2
.= G . p by A32, A37, A39 ;
:: 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] )thus ( p is universal & S5[ the_scope_of p] implies S5[p] ) :: thesis: verum
proof
assume that
A45: p is universal and
A46: S5[ the_scope_of p] and
A47: len (@ p) <= len (@ x9) ; :: thesis: F . p = G . p
len (@ (the_scope_of p)) < len (@ p) by A45, QC_LANG1:14;
hence F . p = F6((G . (the_scope_of p)),p) by A31, A45, A46, A47, XXREAL_0:2
.= G . p by A32, A45, A47 ;
:: thesis: verum
end;
end;
for p being Element of QC-WFF holds S5[p] from QC_LANG1:sch 2(A33);
 hence F . x = G . x9 ; :: thesis: verum
end;
consider F being Function such that
A48: dom F = QC-WFF and
A49: for x being set st x in QC-WFF holds
S4[x,F . x] from CLASSES1:sch 1(A30);
 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
A50: x in QC-WFF and
A51: y = F . x by A48, FUNCT_1:def 3;
consider p being Element of QC-WFF such that
p = x and
A52: for g being Function of QC-WFF,F1() st S1[g, len (@ p)] holds
y = g . p by A49, A50, A51;
consider G being Function of QC-WFF,F1() such that
A53: S1[G, len (@ p)] by A29;
y = G . p by A52, A53;
hence y in F1() ; :: thesis: verum
end;
then reconsider F = F as Function of QC-WFF,F1() by A48, FUNCT_2:def 1, RELSET_1:4;
consider p1 being Element of QC-WFF such that
A54: p1 = VERUM and
A55: for g being Function of QC-WFF,F1() st S1[g, len (@ p1)] holds
F . VERUM = g . p1 by A49;
take F ; :: thesis: ( F . VERUM = F2() & ( for p being Element of QC-WFF holds
( ( p is atomic implies F . p = F3(p) ) & ( p is negative implies F . p = F4((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F6((F . (the_scope_of p)),p) ) ) ) )
consider G being Function of QC-WFF,F1() such that
A56: S1[G, len (@ p1)] by A29;
F . VERUM = G . VERUM by A54, A55, A56;
hence F . VERUM = F2() by A54, A56; :: thesis: for p being Element of QC-WFF holds
( ( p is atomic implies F . p = F3(p) ) & ( p is negative implies F . p = F4((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F6((F . (the_scope_of p)),p) ) )
let p be Element of QC-WFF ; :: thesis: ( ( p is atomic implies F . p = F3(p) ) & ( p is negative implies F . p = F4((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F6((F . (the_scope_of p)),p) ) )
consider p1 being Element of QC-WFF such that
A57: p1 = p and
A58: for g being Function of QC-WFF,F1() st S1[g, len (@ p1)] holds
F . p = g . p1 by A49;
consider G being Function of QC-WFF,F1() such that
A59: S1[G, len (@ p1)] by A29;
set p9 = the_scope_of p;
A60: ex p1 being Element of QC-WFF st
( p1 = the_scope_of p & ( for g being Function of QC-WFF,F1() st S1[g, len (@ p1)] holds
F . (the_scope_of p) = g . p1 ) ) by A49;
A61: F . p = G . p by A57, A58, A59;
hence ( p is atomic implies F . p = F3(p) ) by A57, A59; :: thesis: ( ( p is negative implies F . p = F4((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F6((F . (the_scope_of p)),p) ) )
A62: for k being Element of NAT st k < len (@ p) holds
S1[G,k]
proof
let k be Element of NAT ; :: thesis: ( k < len (@ p) implies S1[G,k] )
assume A63: k < len (@ p) ; :: thesis: S1[G,k]
let p9 be Element of QC-WFF ; :: thesis: ( len (@ p9) <= k implies ( ( p9 = VERUM implies G . p9 = F2() ) & ( p9 is atomic implies G . p9 = F3(p9) ) & ( p9 is negative implies G . p9 = F4((G . (the_argument_of p9)),p9) ) & ( p9 is conjunctive implies G . p9 = F5((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9)),p9) ) & ( p9 is universal implies G . p9 = F6((G . (the_scope_of p9)),p9) ) ) )
assume len (@ p9) <= k ; :: thesis: ( ( p9 = VERUM implies G . p9 = F2() ) & ( p9 is atomic implies G . p9 = F3(p9) ) & ( p9 is negative implies G . p9 = F4((G . (the_argument_of p9)),p9) ) & ( p9 is conjunctive implies G . p9 = F5((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9)),p9) ) & ( p9 is universal implies G . p9 = F6((G . (the_scope_of p9)),p9) ) )
then len (@ p9) <= len (@ p) by A63, XXREAL_0:2;
hence ( ( p9 = VERUM implies G . p9 = F2() ) & ( p9 is atomic implies G . p9 = F3(p9) ) & ( p9 is negative implies G . p9 = F4((G . (the_argument_of p9)),p9) ) & ( p9 is conjunctive implies G . p9 = F5((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9)),p9) ) & ( p9 is universal implies G . p9 = F6((G . (the_scope_of p9)),p9) ) ) by A57, A59; :: thesis: verum
end;
thus ( p is negative implies F . p = F4((F . (the_argument_of p)),p) ) :: thesis: ( ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F6((F . (the_scope_of p)),p) ) )
proof
set p9 = the_argument_of p;
set k = len (@ (the_argument_of p));
A64: ex p1 being Element of QC-WFF st
( p1 = the_argument_of p & ( for g being Function of QC-WFF,F1() st S1[g, len (@ p1)] holds
F . (the_argument_of p) = g . p1 ) ) by A49;
assume A65: p is negative ; :: thesis: F . p = F4((F . (the_argument_of p)),p)
then len (@ (the_argument_of p)) < len (@ p) by QC_LANG1:12;
then S1[G, len (@ (the_argument_of p))] by A62;
then F . (the_argument_of p) = G . (the_argument_of p) by A64;
hence F . p = F4((F . (the_argument_of p)),p) by A57, A59, A61, A65; :: thesis: verum
end;
thus ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) :: thesis: ( p is universal implies F . p = F6((F . (the_scope_of p)),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));
A66: ex p2 being Element of QC-WFF st
( p2 = the_right_argument_of p & ( for g being Function of QC-WFF,F1() st S1[g, len (@ p2)] holds
F . (the_right_argument_of p) = g . p2 ) ) by A49;
assume A67: p is conjunctive ; :: thesis: F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p)
then len (@ (the_left_argument_of p)) < len (@ p) by QC_LANG1:13;
then A68: S1[G, len (@ (the_left_argument_of p))] by A62;
len (@ (the_right_argument_of p)) < len (@ p) by A67, QC_LANG1:13;
then S1[G, len (@ (the_right_argument_of p))] by A62;
then A69: F . (the_right_argument_of p) = G . (the_right_argument_of p) by A66;
ex p1 being Element of QC-WFF st
( p1 = the_left_argument_of p & ( for g being Function of QC-WFF,F1() st S1[g, len (@ p1)] holds
F . (the_left_argument_of p) = g . p1 ) ) by A49;
then F . (the_left_argument_of p) = G . (the_left_argument_of p) by A68;
hence F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) by A57, A59, A61, A67, A69; :: thesis: verum
end;
set k = len (@ (the_scope_of p));
assume A70: p is universal ; :: thesis: F . p = F6((F . (the_scope_of p)),p)
then len (@ (the_scope_of p)) < len (@ p) by QC_LANG1:14;
then S1[G, len (@ (the_scope_of p))] by A62;
then F . (the_scope_of p) = G . (the_scope_of p) by A60;
hence F . p = F6((F . (the_scope_of p)),p) by A57, A59, A61, A70; :: thesis: verum