let D be set ; :: thesis: for s being FinSequence holds
( s is Matrix of D iff 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 ) )
let s be FinSequence; :: thesis: ( s is Matrix of D iff 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 ) )
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: ( 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 ) implies s is Matrix of D )

proof

assume A1: s is Matrix of D ; :: thesis: 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 )
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 )

proof

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

end;

reconsider n = n as Nat ;
take n ; :: thesis: for i being Nat st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n )
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: verum

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: s is Matrix of D
A6: for x being set st x in rng s holds
( ex v being FinSequence st
( v = x & len v = n ) & x in D * )

proof

let x be set ; :: thesis: ( x in rng s implies ( ex v being FinSequence st
( v = x & len v = n ) & x in D * ) )
assume x in rng s ; :: thesis: ( ex v being FinSequence st
( v = x & len v = n ) & x in D * )
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: x in D *
thus x in D * by A8, A9, FINSEQ_1:def 11; :: thesis: verum

end;

then for x being object st x in rng s holds
x in D * ;
then A10: rng s c= D * ;
for x being object st x in rng s holds
ex v being FinSequence st
( v = x & len v = n ) by A6;
hence s is Matrix of D by A10, FINSEQ_1:def 4, MATRIX_0:def 1; :: thesis: verum