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 :: thesis: for y being object holds
( ( 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 ) )

let y be object ; :: 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 object such that
A4: i in dom (rngs M) and
A5: (rngs M) . i = Y by A3, FUNCT_1:def 3;
A6: i in dom M by A4, FUNCT_6:60;
then reconsider i = i as Nat ;
reconsider f = M . i as FinSequence of D by Th34;
A7: Y = rng f by A5, A6, FUNCT_6:22;
A8: f in D * by FINSEQ_1:def 11;
f in rng M by A6, FUNCT_1:def 3;
then rng f in { (rng f) where f is Element of D * : f in rng M } by A8;
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
A9: y in Y and
A10: 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
A11: Y = rng f and
A12: f in rng M by A10;
consider i being Nat such that
A13: ( i in dom M & M . i = f ) by A12, FINSEQ_2:10;
( i in dom (rngs M) & (rngs M) . i = rng f ) by A13, FUNCT_6:22;
then rng f in rng (rngs M) by FUNCT_1:def 3;
hence y in Values M by A1, A9, A11, 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