let k be Element of NAT ; :: thesis: for A being non empty set
for J being interpretation of A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub )
let A be non empty set ; :: thesis: for J being interpretation of A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub )
let J be interpretation of A; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub )
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of k
for Sub being CQC_Substitution
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub )
let ll be CQC-variable_list of k; :: thesis: for Sub being CQC_Substitution
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub )
let Sub be CQC_Substitution; :: thesis: for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub )
set S9 = Sub_P P,ll,Sub;
set ll9 = CQC_Subst ll,Sub;
reconsider p = P ! (CQC_Subst ll,Sub) as Element of CQC-WFF ;
reconsider ll9 = CQC_Subst ll,Sub as CQC-variable_list of k ;
let v be Element of Valuations_in A; :: thesis: ( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub )
A1: ( (Valid p,J) . v = TRUE iff v *' ll9 in J . P ) by VALUAT_1:16;
A2: ( (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll in J . P iff (Valid (P ! ll),J) . (v . (Val_S v,(Sub_P P,ll,Sub))) = TRUE ) by VALUAT_1:16;
A3: ( J,v . (Val_S v,(Sub_P P,ll,Sub)) |= P ! ll iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= (Sub_P P,ll,Sub) `1 ) by Th15;
( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v |= p ) by Th9;
hence ( J,v |= CQC_Sub (Sub_P P,ll,Sub) iff J,v . (Val_S v,(Sub_P P,ll,Sub)) |= Sub_P P,ll,Sub ) by A1, A2, A3, Def3, Th14, VALUAT_1:def 12; :: thesis: verum