thus ex d being Element of F₁() ex F being Function of CQC-WFF ,F₁() st
( d = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) ) :: thesis: for d1, d2 being Element of F₁() st ex F being Function of CQC-WFF ,F₁() st
( d1 = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) ) & ex F being Function of CQC-WFF ,F₁() st
( d2 = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) ) holds
d1 = d2

proof

consider F being Function of CQC-WFF ,F₁() such that
A1: ( F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) ) from CQC_LANG:sch 2();
take F . F₂() ; :: thesis: ex F being Function of CQC-WFF ,F₁() st
( F . F₂() = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) )
take F ; :: thesis: ( F . F₂() = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) )
thus ( F . F₂() = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) ) by A1; :: thesis: verum

end;

let d1, d2 be Element of F₁(); :: thesis: ( ex F being Function of CQC-WFF ,F₁() st
( d1 = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) ) & ex F being Function of CQC-WFF ,F₁() st
( d2 = F . F₂() & F . VERUM = F₃() & ( 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
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₇(x,(F . r)) ) ) ) implies d1 = d2 )
given F1 being Function of CQC-WFF ,F₁() such that A2: d1 = F1 . F₂() and
A3: ( F1 . VERUM = F₃() & ( 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
( F1 . (P ! l) = F₄(k,P,l) & F1 . ('not' r) = F₅((F1 . r)) & F1 . (r '&' s) = F₆((F1 . r),(F1 . s)) & F1 . (All x,r) = F₇(x,(F1 . r)) ) ) ) ; :: thesis: ( for F being Function of CQC-WFF ,F₁() holds
( not d2 = F . F₂() or not F . VERUM = F₃() or ex r, s being Element of CQC-WFF ex x being bound_QC-variable ex k being Element of NAT ex l being CQC-variable_list of ex P being QC-pred_symbol of k st
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) implies not F . (All x,r) = F₇(x,(F . r)) ) ) or d1 = d2 )
given F2 being Function of CQC-WFF ,F₁() such that A4: d2 = F2 . F₂() and
A5: ( F2 . VERUM = F₃() & ( 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
( F2 . (P ! l) = F₄(k,P,l) & F2 . ('not' r) = F₅((F2 . r)) & F2 . (r '&' s) = F₆((F2 . r),(F2 . s)) & F2 . (All x,r) = F₇(x,(F2 . r)) ) ) ) ; :: thesis: d1 = d2
F1 = F2 from CQC_LANG:sch 3(A3, A5);
hence d1 = d2 by A2, A4; :: thesis: verum