let Al be QC-alphabet ; :: thesis: for k being Nat
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,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 k be Nat; :: thesis: for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,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 Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,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 Al,A; :: thesis: for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,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,Al; :: thesis: for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,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,Al; :: thesis: for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,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 of Al; :: thesis: for v being Element of Valuations_in (Al,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 Al ;
reconsider ll9 = CQC_Subst (ll,Sub) as CQC-variable_list of k,Al ;
let v be Element of Valuations_in (Al,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 Th14;
( J,v |= CQC_Sub (Sub_P (P,ll,Sub)) iff J,v |= p ) by Th8;
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, Th13, VALUAT_1:def 7; :: thesis: verum