let Al be QC-alphabet ; :: thesis: for k being Nat
for ll being CQC-variable_list of k,Al holds (valH Al) *' ll = ll
let k be Nat; :: thesis: for ll being CQC-variable_list of k,Al holds (valH Al) *' ll = ll
let ll be CQC-variable_list of k,Al; :: thesis: (valH Al) *' ll = ll
A1: for i being Nat st i in dom ((valH Al) *' ll) holds
(valH Al) . (ll . i) = ll . i
proof
A2: dom ((valH Al) *' ll) c= dom ll by RELAT_1:25;
let i be Nat; :: thesis: ( i in dom ((valH Al) *' ll) implies (valH Al) . (ll . i) = ll . i )
assume i in dom ((valH Al) *' ll) ; :: thesis: (valH Al) . (ll . i) = ll . i
then A3: ll . i in rng ll by A2, FUNCT_1:3;
rng ll c= bound_QC-variables Al by RELAT_1:def 19;
hence (valH Al) . (ll . i) = ll . i by A3, FUNCT_1:18; :: thesis: verum
end;
A4: for i being Nat st 1 <= i & i <= k holds
(valH Al) . (ll . i) = ll . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= k implies (valH Al) . (ll . i) = ll . i )
assume that
A5: 1 <= i and
A6: i <= k ; :: thesis: (valH Al) . (ll . i) = ll . i
i <= len ((valH Al) *' ll) by A6, VALUAT_1:def 3;
then i in dom ((valH Al) *' ll) by A5, FINSEQ_3:25;
hence (valH Al) . (ll . i) = ll . i by A1; :: thesis: verum
end;
A7: len ll = k by CARD_1:def 7;
then A8: dom ll = Seg k by FINSEQ_1:def 3;
A9: for i being Nat st i in dom ll holds
((valH Al) *' ll) . i = ll . i
proof
let i be Nat; :: thesis: ( i in dom ll implies ((valH Al) *' ll) . i = ll . i )
assume A10: i in dom ll ; :: thesis: ((valH Al) *' ll) . i = ll . i
reconsider i = i as Nat ;
A11: ( 1 <= i & i <= k ) by A8, A10, FINSEQ_1:1;
then ((valH Al) *' ll) . i = (valH Al) . (ll . i) by VALUAT_1:def 3;
hence ((valH Al) *' ll) . i = ll . i by A4, A11; :: thesis: verum
end;
len ((valH Al) *' ll) = k by VALUAT_1:def 3;
hence (valH Al) *' ll = ll by A7, A9, FINSEQ_2:9; :: thesis: verum