let p be Element of CQC-WFF ; :: thesis: for A being non empty set
for J being interpretation of A holds
( Valid (VERUM,J) = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let A be non empty set ; :: thesis: for J being interpretation of A holds
( Valid (VERUM,J) = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let J be interpretation of A; :: thesis: ( Valid (VERUM,J) = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
set D = Funcs ((Valuations_in A),BOOLEAN);
set V = (Valuations_in A) --> TRUE;
deffunc H₁( Element of NAT , QC-pred_symbol of $1, CQC-variable_list of $1) -> Element of Funcs ((Valuations_in A),BOOLEAN) = $3 'in' (J . $2);
deffunc H₂( Element of Funcs ((Valuations_in A),BOOLEAN)) -> Element of Funcs ((Valuations_in A),BOOLEAN) = 'not' $1;
deffunc H₃( Element of Funcs ((Valuations_in A),BOOLEAN), Element of Funcs ((Valuations_in A),BOOLEAN)) -> Element of Funcs ((Valuations_in A),BOOLEAN) = $1 '&' $2;
deffunc H₄( bound_QC-variable, Element of Funcs ((Valuations_in A),BOOLEAN)) -> Element of Funcs ((Valuations_in A),BOOLEAN) = FOR_ALL ($1,$2);
deffunc H₅( Element of CQC-WFF ) -> Element of Funcs ((Valuations_in A),BOOLEAN) = Valid ($1,J);
A1: for p being Element of CQC-WFF
for d being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( d = H₅(p) iff ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( d = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! ll) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(x,F . p) ) ) ) ) by Def11;
thus H₅( VERUM ) = (Valuations_in A) --> TRUE from CQC_LANG:sch 5(A1); :: thesis: ( ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )

hereby :: thesis: ( ( for p being Element of CQC-WFF holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )

let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds H₅(P ! ll) = H₁(k,P,ll)
let ll be CQC-variable_list of k; :: thesis: for P being QC-pred_symbol of k holds H₅(P ! ll) = H₁(k,P,ll)
let P be QC-pred_symbol of k; :: thesis: H₅(P ! ll) = H₁(k,P,ll)
thus H₅(P ! ll) = H₁(k,P,ll) from CQC_LANG:sch 6(A1); :: thesis: verum

end;

hereby :: thesis: ( ( for q being Element of CQC-WFF holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )

let p be Element of CQC-WFF ; :: thesis: H₅( 'not' p) = H₂(H₅(p))
thus H₅( 'not' p) = H₂(H₅(p)) from CQC_LANG:sch 7(A1); :: thesis: verum

end;

hereby :: thesis: for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J)))

let q be Element of CQC-WFF ; :: thesis: H₅(p '&' q) = H₃(H₅(p),H₅(q))
thus H₅(p '&' q) = H₃(H₅(p),H₅(q)) from CQC_LANG:sch 8(A1); :: thesis: verum

end;

let x be bound_QC-variable; :: thesis: Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J)))
thus H₅( All (x,p)) = H₄(x,H₅(p)) from CQC_LANG:sch 9(A1); :: thesis: verum