deffunc H₁( 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)));
consider F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that
A1: F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) and
A2: 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
( F . (P ! l) = H₁(k,P,l) & F . ('not' r) = H₂(F . r) & F . (r '&' s) = H₃(F . r,F . s) & F . (All (x,r)) = H₄(x,F . r) ) from CQC_LANG:sch 2();
take F . p ; :: thesis: ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( F . p = 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)) ) ) )
take F ; :: thesis: ( F . p = 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)) ) ) )
thus F . p = F . p ; :: thesis: ( 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)) ) ) )
(Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
hence F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE by A1, SUBSET_1:def 8; :: thesis: 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)) )
let p, q be Element of CQC-WFF Al; :: thesis: 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)) )
let x be bound_QC-variable of Al; :: thesis: 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)) )
let k be Nat; :: thesis: 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)) )
let ll be CQC-variable_list of k,Al; :: thesis: 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)) )
let P be QC-pred_symbol of k,Al; :: thesis: ( 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)) )
thus F . (P ! ll) = ll 'in' (J . P) by A2; :: thesis: ( F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
A3: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . ('not' p) = H₂(F . p) by A2
.= 'not' (F . p) by A3, SUBSET_1:def 8 ; :: thesis: ( F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
A4: (F . p) '&' (F . q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . (p '&' q) = H₃(F . p,F . q) by A2
.= (F . p) '&' (F . q) by A4, SUBSET_1:def 8 ; :: thesis: F . (All (x,p)) = FOR_ALL (x,(F . p))
thus F . (All (x,p)) = H₄(x,F . p) by A2
.= FOR_ALL (x,(F . p)) by SUBSET_1:def 8 ; :: thesis: verum