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 k
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 k
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 k
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 k
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 k; :: 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) by A2;
hence F₃() . (P ! ll) = F₄() . (P ! ll) by A5; :: 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) by A3;
hence ( F₃() . r = F₄() . r implies F₃() . ('not' r) = F₄() . ('not' r) ) by A6; :: 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) by A3;
hence ( F₃() . r = F₄() . r & F₃() . s = F₄() . s implies F₃() . (r '&' s) = F₄() . (r '&' s) ) by A6; :: thesis: ( S₁[r] implies S₁[ All (x,r)] )
F₃() . (All (x,r)) = F₉(x,(F₃() . r),r) by A3;
hence ( S₁[r] implies S₁[ All (x,r)] ) by A6; :: 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:63; :: thesis: verum