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:7;
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:7;
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 7; :: thesis: verum