deffunc H1( 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 H2( 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 H3( 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 H4( 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 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 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 A5: d1 = F1 . p and
A6: F1 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
A7: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(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 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 )
A8: 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 Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) ) )
thus F1 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by A6, SUBSET_1:def 8; :: thesis: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let r, s be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let x be bound_QC-variable of Al; :: thesis: for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let k be Nat; :: thesis: for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(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) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let P be QC-pred_symbol of k,Al; :: thesis: ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
thus F1 . (P ! l) = H1(k,P,l) by A7; :: thesis: ( F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
A9: 'not' (F1 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F1 . ('not' r) = 'not' (F1 . r) by A7
.= H2(F1 . r) by A9, SUBSET_1:def 8 ; :: thesis: ( F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
A10: (F1 . r) '&' (F1 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F1 . (r '&' s) = (F1 . r) '&' (F1 . s) by A7
.= H3(F1 . r,F1 . s) by A10, SUBSET_1:def 8 ; :: thesis: F1 . (All (x,r)) = H4(x,F1 . r)
thus F1 . (All (x,r)) = FOR_ALL (x,(F1 . r)) by A7
.= H4(x,F1 . r) by SUBSET_1:def 8 ; :: thesis: verum
end;
given F2 being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that A11: d2 = F2 . p and
A12: F2 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
A13: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(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
A14: 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 Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) ) )
thus F2 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by A12, SUBSET_1:def 8; :: thesis: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let r, s be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let x be bound_QC-variable of Al; :: thesis: for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let k be Nat; :: thesis: for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(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) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let P be QC-pred_symbol of k,Al; :: thesis: ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
thus F2 . (P ! l) = H1(k,P,l) by A13; :: thesis: ( F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
A15: 'not' (F2 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F2 . ('not' r) = 'not' (F2 . r) by A13
.= H2(F2 . r) by A15, SUBSET_1:def 8 ; :: thesis: ( F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
A16: (F2 . r) '&' (F2 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F2 . (r '&' s) = (F2 . r) '&' (F2 . s) by A13
.= H3(F2 . r,F2 . s) by A16, SUBSET_1:def 8 ; :: thesis: F2 . (All (x,r)) = H4(x,F2 . r)
thus F2 . (All (x,r)) = FOR_ALL (x,(F2 . r)) by A13
.= H4(x,F2 . r) by SUBSET_1:def 8 ; :: thesis: verum
end;
F1 = F2 from CQC_LANG:sch 3(A8, A14);
 hence d1 = d2 by A5, A11; :: thesis: verum