let D be set ; :: thesis:
let s be FinSequence; :: thesis:
thus ( s is Matrix of D implies ex n being Nat st
for i being Nat st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) ) :: thesis:

assume A1: s is Matrix of D ; :: thesis:
then reconsider v = s as FinSequence of D * ;
consider n being Nat such that
A2: for x being object st x in rng v holds
ex t being FinSequence st
( t = x & len t = n ) by A1, MATRIX_0:def 1;
A3: for i being Nat st i in dom v holds
ex p being FinSequence of D st
( v . i = p & len p = n )

let i be Nat; :: thesis:
assume i in dom v ; :: thesis:
then consider t being FinSequence such that
A4: ( t = v . i & len t = n ) by A2, FUNCT_1:3;
take t ; :: thesis:
thus ( t is Element of bool [:NAT,D:] & t is FinSequence of D & v . i = t & len t = n ) by A4; :: thesis:

end;

reconsider n = n as Nat ;
take n ; :: thesis:
thus for i being Nat st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) by A3; :: thesis:

end;

given n being Nat such that A5: for i being Nat st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) ; :: thesis:
A6: for x being set st x in rng s holds
( ex v being FinSequence st
( v = x & len v = n ) & x in D * )

let x be set ; :: thesis:
assume x in rng s ; :: thesis:
then consider i being object such that
A7: i in dom s and
A8: x = s . i by FUNCT_1:def 3;
A9: ex p being FinSequence of D st
( s . i = p & len p = n ) by A5, A7;
hence ex v being FinSequence st
( v = x & len v = n ) by A8; :: thesis:
thus x in D * by A8, A9, FINSEQ_1:def 11; :: thesis:

end;