deffunc H₁( Element of NAT , QC-pred_symbol of $1,Al, CQC-variable_list of $1,Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = $3 'in' (J . $2);
set D = Funcs ((Valuations_in (Al,A)),BOOLEAN);
set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H₂( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (('not' $1),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H₃( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN), Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (($1 '&' $2),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H₄( bound_QC-variable of Al, Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((FOR_ALL ($1,$2)),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
let d1, d2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); :: thesis: ( ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) & ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d2 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) implies d1 = d2 )
given F1 being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that Z1: d1 = F1 . p and
Z2: F1 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
Z3: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = 'not' (F1 . r) & F1 . (r '&' s) = (F1 . r) '&' (F1 . s) & F1 . (All (x,r)) = FOR_ALL (x,(F1 . r)) ) ; :: thesis: ( for F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) holds
( not d2 = F . p or not F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE or ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al ex k being Element of NAT ex ll being CQC-variable_list of k,Al ex P being QC-pred_symbol of k,Al st
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) implies not F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) or d1 = d2 )

Y2: now :: thesis: ( F1 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) ) ) )

thus F1 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by Z2, FUNCT_7:def 1; :: thesis: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
let r, s be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
let x be bound_QC-variable of Al; :: thesis: for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
let k be Element of NAT ; :: thesis: for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
let l be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
let P be QC-pred_symbol of k,Al; :: thesis: ( F1 . (P ! l) = H₁(k,P,l) & F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
thus F1 . (P ! l) = H₁(k,P,l) by Z3; :: thesis: ( F1 . ('not' r) = H₂(F1 . r) & F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
X1: 'not' (F1 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F1 . ('not' r) = 'not' (F1 . r) by Z3
.= H₂(F1 . r) by X1, FUNCT_7:def 1 ; :: thesis: ( F1 . (r '&' s) = H₃(F1 . r,F1 . s) & F1 . (All (x,r)) = H₄(x,F1 . r) )
X1: (F1 . r) '&' (F1 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F1 . (r '&' s) = (F1 . r) '&' (F1 . s) by Z3
.= H₃(F1 . r,F1 . s) by X1, FUNCT_7:def 1 ; :: thesis: F1 . (All (x,r)) = H₄(x,F1 . r)
thus F1 . (All (x,r)) = FOR_ALL (x,(F1 . r)) by Z3
.= H₄(x,F1 . r) by FUNCT_7:def 1 ; :: thesis: verum

end;

given F2 being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that Z4: d2 = F2 . p and
Z5: F2 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
Z6: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = 'not' (F2 . r) & F2 . (r '&' s) = (F2 . r) '&' (F2 . s) & F2 . (All (x,r)) = FOR_ALL (x,(F2 . r)) ) ; :: thesis: d1 = d2

Y5: now :: thesis: ( F2 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) ) ) )

thus F2 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by Z5, FUNCT_7:def 1; :: thesis: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
let r, s be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
let x be bound_QC-variable of Al; :: thesis: for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
let k be Element of NAT ; :: thesis: for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
let l be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
let P be QC-pred_symbol of k,Al; :: thesis: ( F2 . (P ! l) = H₁(k,P,l) & F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
thus F2 . (P ! l) = H₁(k,P,l) by Z6; :: thesis: ( F2 . ('not' r) = H₂(F2 . r) & F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
X1: 'not' (F2 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F2 . ('not' r) = 'not' (F2 . r) by Z6
.= H₂(F2 . r) by X1, FUNCT_7:def 1 ; :: thesis: ( F2 . (r '&' s) = H₃(F2 . r,F2 . s) & F2 . (All (x,r)) = H₄(x,F2 . r) )
X1: (F2 . r) '&' (F2 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F2 . (r '&' s) = (F2 . r) '&' (F2 . s) by Z6
.= H₃(F2 . r,F2 . s) by X1, FUNCT_7:def 1 ; :: thesis: F2 . (All (x,r)) = H₄(x,F2 . r)
thus F2 . (All (x,r)) = FOR_ALL (x,(F2 . r)) by Z6
.= H₄(x,F2 . r) by FUNCT_7:def 1 ; :: thesis: verum

end;

F1 = F2 from CQC_LANG:sch 3(Y2, Y5);
hence d1 = d2 by Z1, Z4; :: thesis: verum