let Al be QC-alphabet ; :: thesis: for k being Nat
for A being non empty set
for v being Element of Valuations_in (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 holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))
let k be Nat; :: thesis: for A being non empty set
for v being Element of Valuations_in (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 holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))
let A be non empty set ; :: thesis: for v being Element of Valuations_in (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 holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))
let v be Element of Valuations_in (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 holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (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 holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))
let ll be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))
let Sub be CQC_Substitution of Al; :: thesis: (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))
set S9 = Sub_P (P,ll,Sub);
set ll9 = CQC_Subst (ll,Sub);
A1: len ll = k by CARD_1:def 7;
Sub_P (P,ll,Sub) = [(P ! ll),Sub] by SUBSTUT1:9;
then A2: (Sub_P (P,ll,Sub)) `2 = Sub ;
A3: len ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) = k by VALUAT_1:def 3;
then A4: dom ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) = Seg k by FINSEQ_1:def 3;
A5: for j being Nat st j in dom ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) holds
((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j
proof
let j be Nat; :: thesis: ( j in dom ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) implies ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j )
assume A6: j in dom ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) ; :: thesis: ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j
A7: ( 1 <= j & j <= k ) by A4, A6, FINSEQ_1:1;
reconsider j = j as Nat ;
j in Seg (len ll) by A4, A6, CARD_1:def 7;
then j in dom ll by FINSEQ_1:def 3;
then reconsider x = ll . j as bound_QC-variable of Al by Th5;
A8: now :: thesis: ( ll . j in dom Sub implies ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j )
assume A9: ll . j in dom Sub ; :: thesis: ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j
then ( (v . (Val_S (v,(Sub_P (P,ll,Sub))))) . (ll . j) = (Val_S (v,(Sub_P (P,ll,Sub)))) . x & ll . j in dom (@ ((Sub_P (P,ll,Sub)) `2)) ) by A2, Th12, SUBSTUT1:def 2;
then (v . (Val_S (v,(Sub_P (P,ll,Sub))))) . (ll . j) = v . ((@ ((Sub_P (P,ll,Sub)) `2)) . (ll . j)) by FUNCT_1:13;
then A10: (v . (Val_S (v,(Sub_P (P,ll,Sub))))) . (ll . j) = v . (((Sub_P (P,ll,Sub)) `2) . (ll . j)) by SUBSTUT1:def 2;
A11: ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v . (Val_S (v,(Sub_P (P,ll,Sub))))) . (ll . j) by A7, VALUAT_1:def 3;
v . ((CQC_Subst (ll,Sub)) . j) = v . (((Sub_P (P,ll,Sub)) `2) . (ll . j)) by A2, A1, A7, A9, SUBSTUT1:def 3;
hence ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j by A7, A10, A11, VALUAT_1:def 3; :: thesis: verum
end;
now :: thesis: ( not ll . j in dom Sub implies ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j )
assume not ll . j in dom Sub ; :: thesis: ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j
then A12: ( v . ((CQC_Subst (ll,Sub)) . j) = v . (ll . j) & (v . (Val_S (v,(Sub_P (P,ll,Sub))))) . (ll . j) = v . x ) by A2, A1, A7, Th11, SUBSTUT1:def 3;
(v *' (CQC_Subst (ll,Sub))) . j = v . ((CQC_Subst (ll,Sub)) . j) by A7, VALUAT_1:def 3;
hence ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j by A7, A12, VALUAT_1:def 3; :: thesis: verum
end;
hence ((v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll) . j = (v *' (CQC_Subst (ll,Sub))) . j by A8; :: thesis: verum
end;
len (v *' (CQC_Subst (ll,Sub))) = k by VALUAT_1:def 3;
hence (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub)) by A3, A5, FINSEQ_2:9; :: thesis: verum