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
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
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
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
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 ; :: 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 S' = Sub_P P,ll,Sub;
Sub_P P,ll,Sub = [(P ! ll),Sub] by SUBSTUT1:9;
then A1: (Sub_P P,ll,Sub) `2 = Sub by MCART_1:7;
set ll' = CQC_Subst ll,Sub;
A2: len ll = k by FINSEQ_1:def 18;
Y: len (v *' (CQC_Subst ll,Sub)) = k by VALUAT_1:def 8;
A14: len ((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) = k by VALUAT_1:def 8;
then X: dom ((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) = Seg k by FINSEQ_1:def 3;
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 A4: 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
A5: ( 1 <= j & j <= k ) by A4, X, FINSEQ_1:3;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j in Seg (len ll) by A4, X, 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;

A6: now

assume A7: 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 A8: v . ((CQC_Subst ll,Sub) . j) = v . (ll . j) by A2, A5, SUBSTUT1:def 3;
A9: (v *' (CQC_Subst ll,Sub)) . j = v . ((CQC_Subst ll,Sub) . j) by A5, VALUAT_1:def 8;
(v . (Val_S v,(Sub_P P,ll,Sub))) . (ll . j) = v . x by A1, A7, Th12;
hence ((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) . j = (v *' (CQC_Subst ll,Sub)) . j by A5, A8, A9, VALUAT_1:def 8; :: thesis: verum

end;

now

assume A10: ll . j in dom Sub ; :: thesis: ((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) . j = (v *' (CQC_Subst ll,Sub)) . j
then A11: v . ((CQC_Subst ll,Sub) . j) = v . (((Sub_P P,ll,Sub) `2 ) . (ll . j)) by A1, A2, A5, SUBSTUT1:def 3;
A12: (v . (Val_S v,(Sub_P P,ll,Sub))) . (ll . j) = (Val_S v,(Sub_P P,ll,Sub)) . x by A1, A10, Th13;
ll . j in dom (@ ((Sub_P P,ll,Sub) `2 )) by A1, A10, 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 A12, FUNCT_1:23;
then A13: (v . (Val_S v,(Sub_P P,ll,Sub))) . (ll . j) = v . (((Sub_P P,ll,Sub) `2 ) . (ll . j)) by SUBSTUT1:def 2;
((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) . j = (v . (Val_S v,(Sub_P P,ll,Sub))) . (ll . j) by A5, VALUAT_1:def 8;
hence ((v . (Val_S v,(Sub_P P,ll,Sub))) *' ll) . j = (v *' (CQC_Subst ll,Sub)) . j by A5, A11, A13, 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 A6; :: thesis: verum

end;

hence (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll = v *' (CQC_Subst ll,Sub) by A14, Y, FINSEQ_2:10; :: thesis: verum