let D be non empty set ; :: thesis:
let s be FinSequence; :: thesis:
thus ( s is Matrix of D implies ex n being Nat st
for x being object st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) ) :: thesis:

assume s is Matrix of D ; :: thesis:
then reconsider s = s as tabular FinSequence of D * ;
consider n being Nat such that
A1: for x being object st x in rng s holds
ex t being FinSequence st
( t = x & len t = n ) by Def1;
take n ; :: thesis:
for x being object st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n )

let x be object ; :: thesis:
assume A2: x in rng s ; :: thesis:
then consider v being FinSequence such that
A3: v = x and
A4: len v = n by A1;
rng s c= D * by FINSEQ_1:def 4;
then reconsider p = v as FinSequence of D by A2, A3, FINSEQ_1:def 11;
take p ; :: thesis:
thus ( x = p & len p = n ) by A3, A4; :: thesis:

end;

hence for x being object st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) ; :: thesis:

end;

given n being Nat such that A5: for x being object st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) ; :: thesis:
A6: s is tabular

consider n being Nat such that
A7: for x being object st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) by A5;
take n ; :: according to MATRIX_0:def 1 :: thesis:
for x being object st x in rng s holds
ex t being FinSequence st
( t = x & len t = n )

let x be object ; :: thesis:
assume x in rng s ; :: thesis:
then consider p being FinSequence of D such that
A8: ( x = p & len p = n ) by A7;
reconsider t = p as FinSequence ;
take t ; :: thesis:
thus ( t = x & len t = n ) by A8; :: thesis:

end;

hence for x being object st x in rng s holds
ex s being FinSequence st
( s = x & len s = n ) ; :: thesis:

end;

rng s c= D *

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng s ; :: thesis:
then ex p being FinSequence of D st
( x = p & len p = n ) by A5;
then reconsider q = x as FinSequence of D ;
q in D * by FINSEQ_1:def 11;
hence x in D * ; :: thesis:

end;