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

proof

thus dom (valH *' ll) = dom ll :: thesis: for i being Element of NAT st i in dom (valH *' ll) holds
valH . (ll . i) = ll . i

proof

thus dom (valH *' ll) c= dom ll by RELAT_1:44; :: according to XBOOLE_0:def 10 :: thesis: dom ll c= dom (valH *' ll)
thus dom ll c= dom (valH *' ll) :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in dom ll or a in dom (valH *' ll) )
assume A2: a in dom ll ; :: thesis: a in dom (valH *' ll)
reconsider i = a as Element of NAT by A2;
A3: ll . i in rng ll by A2, FUNCT_1:12;
rng ll c= bound_QC-variables by RELAT_1:def 19;
then ll . i in bound_QC-variables by A3;
then ll . i in dom (id bound_QC-variables ) by RELAT_1:71;
hence a in dom (valH *' ll) by A2, FUNCT_1:21; :: thesis: verum

end;

end;

thus for i being Element of NAT st i in dom (valH *' ll) holds
valH . (ll . i) = ll . i :: thesis: verum

proof

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

end;

end;

A6: 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 A7: ( 1 <= i & i <= k ) ; :: thesis: valH . (ll . i) = ll . i
( 1 <= i & i <= len (valH *' ll) ) by A7, VALUAT_1:def 8;
then i in dom (valH *' ll) by FINSEQ_3:27;
hence valH . (ll . i) = ll . i by A1; :: thesis: verum

end;

A8: ( len (valH *' ll) = k & len ll = k ) by FINSEQ_1:def 18, VALUAT_1:def 8;
then X: dom ll = Seg k by FINSEQ_1:def 3;
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 A9: i in dom ll ; :: thesis: (valH *' ll) . i = ll . i
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A10: ( 1 <= i & i <= k ) by A9, X, FINSEQ_1:3;
then (valH *' ll) . i = valH . (ll . i) by VALUAT_1:def 8;
hence (valH *' ll) . i = ll . i by A6, A10; :: thesis: verum

end;

hence valH *' ll = ll by A8, FINSEQ_2:10; :: thesis: verum