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
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
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
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
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 ; :: 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) & F₃() . (P ! l) = F₅(k,P,l) ) by A1, A2;
hence F₂() . (P ! l) = F₃() . (P ! l) ; :: 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)) & F₃() . ('not' r) = F₆((F₃() . r)) ) by A1, A2;
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)) & F₃() . (r '&' s) = F₇((F₃() . r),(F₃() . s)) ) by A1, A2;
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)) & F₃() . (All x,r) = F₈(x,(F₃() . r)) ) by A1, A2;
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(A3);
hence F₂() = F₃() by FUNCT_2:113; :: thesis: verum