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

(valH Al) . (ll . i) = ll . i

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

hence (valH Al) *' ll = ll by A7, A9, FINSEQ_2:9; :: thesis: verum

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

A4:
for i being Nat st 1 <= i & i <= k holds
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;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

(valH Al) . (ll . i) = ll . i

proof

A7:
len ll = k
by CARD_1:def 7;
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;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

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

len ((valH Al) *' ll) = k
by VALUAT_1:def 3;
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;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

hence (valH Al) *' ll = ll by A7, A9, FINSEQ_2:9; :: thesis: verum