let D be non empty set ; :: thesis: for f being FinSequence of D * holds rng ((D -concatenation) "**" f) = Values f
let f be FinSequence of D * ; :: thesis: rng ((D -concatenation) "**" f) = Values f
set DC = D -concatenation ;
defpred S₁[ Nat] means for f being FinSequence of D * st len f = $1 holds
rng ((D -concatenation) "**" f) = Values f;
A1: S₁[ 0 ]

proof

let f be FinSequence of D * ; :: thesis: ( len f = 0 implies rng ((D -concatenation) "**" f) = Values f )
assume A2: len f = 0 ; :: thesis: rng ((D -concatenation) "**" f) = Values f
A3: f = {} by A2;
then (D -concatenation) "**" f = {} by Lm1;
then A4: rng ((D -concatenation) "**" f) = {} ;
assume rng ((D -concatenation) "**" f) <> Values f ; :: thesis: contradiction
then consider a being object such that
A5: a in Values f by A4, XBOOLE_0:def 1;
ex x, y being object st
( x in dom f & y in dom (f . x) & a = (f . x) . y ) by A5, Th1;
hence contradiction by A3; :: thesis: verum

end;

A6: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
let f1 be FinSequence of D * ; :: thesis: ( len f1 = i + 1 implies rng ((D -concatenation) "**" f1) = Values f1 )
assume A8: len f1 = i + 1 ; :: thesis: rng ((D -concatenation) "**" f1) = Values f1
consider f being FinSequence of D * , d being Element of D * such that
A9: f1 = f ^ <*d*> by FINSEQ_2:19, A8;
(len f) + 1 = len f1 by A9, FINSEQ_2:16;
then A10: rng ((D -concatenation) "**" f) = Values f by A8, A7;
(D -concatenation) "**" f1 = ((D -concatenation) "**" f) ^ ((D -concatenation) "**" <*d*>) by Th3, A9
.= ((D -concatenation) "**" f) ^ d by FINSOP_1:11 ;
then A11: rng ((D -concatenation) "**" f1) = (rng ((D -concatenation) "**" f)) \/ (rng d) by FINSEQ_1:31;
A12: rngs <*d*> = <*(rng d)*> by FINSEQ_3:132;
rng <*(rng d)*> = {(rng d)} by FINSEQ_1:38;
then union (rng <*(rng d)*>) = rng d by ZFMISC_1:25;
then Union (rngs <*d*>) = rng d by CARD_3:def 4, A12;
then Values <*d*> = rng d by MATRIX_0:def 9;
hence rng ((D -concatenation) "**" f1) = Values f1 by Th2, A9, A10, A11; :: thesis: verum

end;

A13: for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A6);
S₁[ len f] by A13;
hence rng ((D -concatenation) "**" f) = Values f ; :: thesis: verum