let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of k holds valH *' ll = ll
let ll be CQC-variable_list of k; :: thesis: valH *' ll = ll
A1: for i being Element of NAT st i in dom (valH *' ll) holds
valH . (ll . i) = ll . i

proof

A2: dom (valH *' ll) c= dom ll by RELAT_1:44;
let i be Element of NAT ; :: thesis: ( i in dom (valH *' ll) implies valH . (ll . i) = ll . i )
assume i in dom (valH *' ll) ; :: thesis: valH . (ll . i) = ll . i
then A3: ll . i in rng ll by A2, FUNCT_1:12;
rng ll c= bound_QC-variables by RELAT_1:def 19;
hence valH . (ll . i) = ll . i by A3, FUNCT_1:35; :: thesis: verum

end;

A4: for i being Element of NAT st 1 <= i & i <= k holds
valH . (ll . i) = ll . i

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= k implies valH . (ll . i) = ll . i )
assume that
A5: 1 <= i and
A6: i <= k ; :: thesis: valH . (ll . i) = ll . i
i <= len (valH *' ll) by A6, VALUAT_1:def 8;
then i in dom (valH *' ll) by A5, FINSEQ_3:27;
hence valH . (ll . i) = ll . i by A1; :: thesis: verum

end;

A7: len ll = k by FINSEQ_1:def 18;
then A8: dom ll = Seg k by FINSEQ_1:def 3;
A9: for i being Nat st i in dom ll holds
(valH *' ll) . i = ll . i

proof

let i be Nat; :: thesis: ( i in dom ll implies (valH *' ll) . i = ll . i )
assume A10: i in dom ll ; :: thesis: (valH *' ll) . i = ll . i
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A11: ( 1 <= i & i <= k ) by A8, A10, FINSEQ_1:3;
then (valH *' ll) . i = valH . (ll . i) by VALUAT_1:def 8;
hence (valH *' ll) . i = ll . i by A4, A11; :: thesis: verum

end;

len (valH *' ll) = k by VALUAT_1:def 8;
hence valH *' ll = ll by A7, A9, FINSEQ_2:10; :: thesis: verum