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 ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let k be Nat; :: thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let v be Element of Valuations_in (Al,A); :: thesis: for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let ll be CQC-variable_list of k,Al; :: thesis: v *' ll = ll * (v | (still_not-bound_in ll))
rng ll c= bound_QC-variables Al by RELAT_1:def 19;
then A1: rng ll = still_not-bound_in ll by Th57;
dom (v | (still_not-bound_in ll)) = (dom v) /\ (still_not-bound_in ll) by RELAT_1:61;
then dom (v | (still_not-bound_in ll)) = (bound_QC-variables Al) /\ (still_not-bound_in ll) by Th58;
then rng ll = dom (v | (still_not-bound_in ll)) by A1, XBOOLE_1:28;
then A2: dom (ll * (v | (still_not-bound_in ll))) = dom ll by RELAT_1:27;
then A3: dom (ll * (v | (still_not-bound_in ll))) = Seg (len ll) by FINSEQ_1:def 3;
then reconsider f = ll * (v | (still_not-bound_in ll)) as FinSequence by FINSEQ_1:def 2;
len f = len ll by A3, FINSEQ_1:def 3;
then A4: len f = k by SUBSTUT1:34;
then A5: dom f = Seg k by FINSEQ_1:def 3;
A6: for j being Nat st j in dom f holds
f . j = (v *' ll) . j

proof

A7: rng ll c= bound_QC-variables Al by RELAT_1:def 19;
let j be Nat; :: thesis: ( j in dom f implies f . j = (v *' ll) . j )
assume A8: j in dom f ; :: thesis: f . j = (v *' ll) . j
reconsider j = j as Nat ;
ll . j in rng ll by A2, A8, FUNCT_1:3;
then ll . j in bound_QC-variables Al by A7;
then A9: ll . j in dom v by Th58;
ll . j in still_not-bound_in ll by A1, A2, A8, FUNCT_1:3;
then ll . j in (dom v) /\ (still_not-bound_in ll) by A9, XBOOLE_0:def 4;
then A10: (v | (still_not-bound_in ll)) . (ll . j) = v . (ll . j) by FUNCT_1:48;
( 1 <= j & j <= k ) by A5, A8, FINSEQ_1:1;
then (v | (still_not-bound_in ll)) . (ll . j) = (v *' ll) . j by A10, VALUAT_1:def 3;
hence f . j = (v *' ll) . j by A2, A8, FUNCT_1:13; :: thesis: verum

end;

len (v *' ll) = k by VALUAT_1:def 3;
hence v *' ll = ll * (v | (still_not-bound_in ll)) by A4, A6, FINSEQ_2:9; :: thesis: verum