defpred S₁[ set ] means F₂() . $1 = F₃() . $1;
A3: for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! l] & ( 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 bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) )
let x be bound_QC-variable; :: thesis: for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! l] & ( 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 l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) )
let l be CQC-variable_list of k; :: thesis: for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! l] & ( 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 ! l] & ( 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, A2; :: thesis: ( S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) )
F₂() . (P ! l) = F₅(k,P,l) by A1;
hence F₂() . (P ! l) = F₃() . (P ! l) by A2; :: 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)) by A1;
hence ( F₂() . r = F₃() . r implies F₂() . ('not' r) = F₃() . ('not' r) ) by A2; :: thesis: ( ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) )
F₂() . (r '&' s) = F₇((F₂() . r),(F₂() . s)) by A1;
hence ( F₂() . r = F₃() . r & F₂() . s = F₃() . s implies F₂() . (r '&' s) = F₃() . (r '&' s) ) by A2; :: thesis: ( S₁[r] implies S₁[ All (x,r)] )
F₂() . (All (x,r)) = F₈(x,(F₂() . r)) by A1;
hence ( S₁[r] implies S₁[ All (x,r)] ) by A2; :: thesis: verum

end;

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