defpred S_{1}[ set ] means F_{4}() . $1 = F_{5}() . $1;

A7: for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Nat

for ll being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( S_{1}[ VERUM F_{1}()] & S_{1}[P ! ll] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )
_{1}() holds S_{1}[r]
from CQC_LANG:sch 1(A7);

hence F_{4}() = F_{5}()
by FUNCT_2:63; :: thesis: verum

A7: for r, s being Element of CQC-WFF F

for x being bound_QC-variable of F

for k being Nat

for ll being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( S

proof

for r being Element of CQC-WFF F
let r, s be Element of CQC-WFF F_{1}(); :: thesis: for x being bound_QC-variable of F_{1}()

for k being Nat

for ll being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( S_{1}[ VERUM F_{1}()] & S_{1}[P ! ll] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

let x be Element of bound_QC-variables F_{1}(); :: thesis: for k being Nat

for ll being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( S_{1}[ VERUM F_{1}()] & S_{1}[P ! ll] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

let k be Nat; :: thesis: for ll being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( S_{1}[ VERUM F_{1}()] & S_{1}[P ! ll] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

let ll be CQC-variable_list of k,F_{1}(); :: thesis: for P being QC-pred_symbol of k,F_{1}() holds

( S_{1}[ VERUM F_{1}()] & S_{1}[P ! ll] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

let P be QC-pred_symbol of k,F_{1}(); :: thesis: ( S_{1}[ VERUM F_{1}()] & S_{1}[P ! ll] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

thus F_{4}() . (VERUM F_{1}()) = F_{5}() . (VERUM F_{1}())
by A1, A4; :: thesis: ( S_{1}[P ! ll] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

reconsider k = k as Element of NAT by ORDINAL1:def 12;

reconsider l1 = ll as CQC-variable_list of k,F_{1}() ;

F_{4}() . (P ! l1) = F_{7}(k,P,l1)
by A2;

hence F_{4}() . (P ! ll) = F_{5}() . (P ! ll)
by A5; :: thesis: ( ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

F_{4}() . ('not' r) = F_{8}((F_{4}() . r),r)
by A3;

hence ( F_{4}() . r = F_{5}() . r implies F_{4}() . ('not' r) = F_{5}() . ('not' r) )
by A6; :: thesis: ( ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )

F_{4}() . (r '&' s) = F_{9}((F_{4}() . r),(F_{4}() . s),r,s)
by A3;

hence ( F_{4}() . r = F_{5}() . r & F_{4}() . s = F_{5}() . s implies F_{4}() . (r '&' s) = F_{5}() . (r '&' s) )
by A6; :: thesis: ( S_{1}[r] implies S_{1}[ All (x,r)] )

F_{4}() . (All (x,r)) = F_{10}(x,(F_{4}() . r),r)
by A3;

hence ( S_{1}[r] implies S_{1}[ All (x,r)] )
by A6; :: thesis: verum

end;for k being Nat

for ll being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( S

let x be Element of bound_QC-variables F

for ll being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( S

let k be Nat; :: thesis: for ll being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( S

let ll be CQC-variable_list of k,F

( S

let P be QC-pred_symbol of k,F

thus F

reconsider k = k as Element of NAT by ORDINAL1:def 12;

reconsider l1 = ll as CQC-variable_list of k,F

F

hence F

F

hence ( F

F

hence ( F

F

hence ( S

hence F