defpred S₁[ set ] means F₃() . $1 = F₄() . $1;
A7: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )

proof

let r, s be Element of CQC-WFF ; :: thesis: for x being Element of bound_QC-variables
for k being Element of NAT
for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
let x be Element of bound_QC-variables ; :: thesis: for k being Element of NAT
for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
let ll be CQC-variable_list of ; :: thesis: for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
let P be QC-pred_symbol of k; :: thesis: ( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
thus F₃() . VERUM = F₄() . VERUM by A1, A4; :: thesis: ( S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
( F₃() . (P ! ll) = F₆(k,P,ll) & F₄() . (P ! ll) = F₆(k,P,ll) ) by A2, A5;
hence F₃() . (P ! ll) = F₄() . (P ! ll) ; :: thesis: ( ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
( F₃() . ('not' r) = F₇((F₃() . r),r) & F₄() . ('not' r) = F₇((F₄() . r),r) ) by A3, A6;
hence ( F₃() . r = F₄() . r implies F₃() . ('not' r) = F₄() . ('not' r) ) ; :: thesis: ( ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) )
( F₃() . (r '&' s) = F₈((F₃() . r),(F₃() . s),r,s) & F₄() . (r '&' s) = F₈((F₄() . r),(F₄() . s),r,s) ) by A3, A6;
hence ( F₃() . r = F₄() . r & F₃() . s = F₄() . s implies F₃() . (r '&' s) = F₄() . (r '&' s) ) ; :: thesis: ( S₁[r] implies S₁[ All x,r] )
( F₃() . (All x,r) = F₉(x,(F₃() . r),r) & F₄() . (All x,r) = F₉(x,(F₄() . r),r) ) by A3, A6;
hence ( S₁[r] implies S₁[ All x,r] ) ; :: thesis: verum

end;

for r being Element of CQC-WFF holds S₁[r] from CQC_LANG:sch 1(A7);
hence F₃() = F₄() by FUNCT_2:113; :: thesis: verum