let k be Element of NAT ; :: thesis: for A being non empty set
for v being Element of Valuations_in A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution 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 A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll = v *' (CQC_Subst ll,Sub)
let v be Element of Valuations_in A; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll = v *' (CQC_Subst ll,Sub)
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll = v *' (CQC_Subst ll,Sub)
let ll be CQC-variable_list of k; :: thesis: for Sub being CQC_Substitution holds (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll = v *' (CQC_Subst ll,Sub)
let Sub be CQC_Substitution; :: 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 FINSEQ_1:def 18;
Sub_P P,ll,Sub = [(P ! ll),Sub] by SUBSTUT1:9;
then A2: (Sub_P P,ll,Sub) `2 = Sub by MCART_1:7;
A3: len ((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) = k by VALUAT_1:def 8;
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:3;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j in Seg (len ll) by A4, A6, FINSEQ_1:def 18;
then j in dom ll by FINSEQ_1:def 3;
then reconsider x = ll . j as bound_QC-variable by Th5;

A8: now

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, Th13, 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:23;
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 8;
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 8; :: thesis: verum

end;

now

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, Th12, SUBSTUT1:def 3;
(v *' (CQC_Subst ll,Sub)) . j = v . ((CQC_Subst ll,Sub) . j) by A7, VALUAT_1:def 8;
hence ((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) . j = (v *' (CQC_Subst ll,Sub)) . j by A7, A12, VALUAT_1:def 8; :: 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 8;
hence (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll = v *' (CQC_Subst ll,Sub) by A3, A5, FINSEQ_2:10; :: thesis: verum