thus ex d being Element of F₂() ex F being Function of (CQC-WFF F₁()),F₂() st
( d = F . F₃() & F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() st
( d1 = F . F₃() & F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() st
( d2 = F . F₃() & F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() such that
A1: ( F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() st
( F . F₃() = F . F₃() & F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() st
( d1 = F . F₃() & F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() st
( d2 = F . F₃() & F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() such that A2: d1 = F1 . F₃() and
A3: ( F1 . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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₁()),F₂() holds
( not d2 = F . F₃() or not F . (VERUM F₁()) = F₄() or ex r, s being Element of CQC-WFF F₁() ex x being bound_QC-variable of F₁() ex k being Nat ex l being CQC-variable_list of k,F₁() ex P being QC-pred_symbol of k,F₁() 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₁()),F₂() such that A4: d2 = F2 . F₃() and
A5: ( F2 . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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