let D be non empty set ; :: thesis: for M being FinSequence of D * holds Values M = union { (rng f) where f is Element of D * : f in rng M }
let M be FinSequence of D * ; :: thesis: Values M = union { (rng f) where f is Element of D * : f in rng M }
set R = { (rng f) where f is Element of D * : f in rng M } ;
A1: Union (rngs M) = union (rng (rngs M)) by CARD_3:def 4;

now

let y be set ; :: thesis: ( ( y in Values M implies y in union { (rng f) where f is Element of D * : f in rng M } ) & ( y in union { (rng f) where f is Element of D * : f in rng M } implies y in Values M ) )

hereby :: thesis: ( y in union { (rng f) where f is Element of D * : f in rng M } implies y in Values M )

assume y in Values M ; :: thesis: y in union { (rng f) where f is Element of D * : f in rng M }
then consider Y being set such that
A2: y in Y and
A3: Y in rng (rngs M) by A1, TARSKI:def 4;
consider i being set such that
A4: i in dom (rngs M) and
A5: (rngs M) . i = Y by A3, FUNCT_1:def 5;
A6: i in dom M by A4, FUNCT_6:90;
then reconsider i = i as Element of NAT ;
reconsider f = M . i as FinSequence of D by Th1;
( f in rng M & f in D * ) by A6, FINSEQ_1:def 11, FUNCT_1:def 5;
then A7: rng f in { (rng f) where f is Element of D * : f in rng M } ;
Y = rng f by A5, A6, FUNCT_6:31;
hence y in union { (rng f) where f is Element of D * : f in rng M } by A2, A7, TARSKI:def 4; :: thesis: verum

end;

assume y in union { (rng f) where f is Element of D * : f in rng M } ; :: thesis: y in Values M
then consider Y being set such that
A8: y in Y and
A9: Y in { (rng f) where f is Element of D * : f in rng M } by TARSKI:def 4;
consider f being Element of D * such that
A10: Y = rng f and
A11: f in rng M by A9;
consider i being Nat such that
A12: i in dom M and
A13: M . i = f by A11, FINSEQ_2:11;
( i in dom (rngs M) & (rngs M) . i = rng f ) by A12, A13, FUNCT_6:31;
then rng f in rng (rngs M) by FUNCT_1:def 5;
hence y in Values M by A1, A8, A10, TARSKI:def 4; :: thesis: verum

end;

hence Values M = union { (rng f) where f is Element of D * : f in rng M } by TARSKI:2; :: thesis: verum