thus ex d being Element of F2() ex F being Function of (CQC-WFF F1()),F2() st
( d = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) :: thesis: for d1, d2 being Element of F2() st ex F being Function of (CQC-WFF F1()),F2() st
( d1 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ex F being Function of (CQC-WFF F1()),F2() st
( d2 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) holds
d1 = d2
proof
consider F being Function of (CQC-WFF F1()),F2() such that
A1: ( F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) from CQC_LANG:sch 2();
 take F . F3() ; :: thesis: ex F being Function of (CQC-WFF F1()),F2() st
( F . F3() = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) )
take F ; :: thesis: ( F . F3() = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) )
thus ( F . F3() = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) by A1; :: thesis: verum
end;
let d1, d2 be Element of F2(); :: thesis: ( ex F being Function of (CQC-WFF F1()),F2() st
( d1 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ex F being Function of (CQC-WFF F1()),F2() st
( d2 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) implies d1 = d2 )
given F1 being Function of (CQC-WFF F1()),F2() such that A2: d1 = F1 . F3() and
A3: ( F1 . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F1 . (P ! l) = F5(k,P,l) & F1 . ('not' r) = F6((F1 . r)) & F1 . (r '&' s) = F7((F1 . r),(F1 . s)) & F1 . (All (x,r)) = F8(x,(F1 . r)) ) ) ) ; :: thesis: ( for F being Function of (CQC-WFF F1()),F2() holds
( not d2 = F . F3() or not F . (VERUM F1()) = F4() or ex r, s being Element of CQC-WFF F1() ex x being bound_QC-variable of F1() ex k being Nat ex l being CQC-variable_list of k,F1() ex P being QC-pred_symbol of k,F1() st
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) implies not F . (All (x,r)) = F8(x,(F . r)) ) ) or d1 = d2 )
given F2 being Function of (CQC-WFF F1()),F2() such that A4: d2 = F2 . F3() and
A5: ( F2 . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F2 . (P ! l) = F5(k,P,l) & F2 . ('not' r) = F6((F2 . r)) & F2 . (r '&' s) = F7((F2 . r),(F2 . s)) & F2 . (All (x,r)) = F8(x,(F2 . r)) ) ) ) ; :: thesis: d1 = d2
F1 = F2 from CQC_LANG:sch 3(A3, A5);
 hence d1 = d2 by A2, A4; :: thesis: verum