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

proof

assume s is Matrix of D ; :: thesis: 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 )
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 )
for x being object st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n )

proof

let x be object ; :: thesis: ( x in rng s implies ex p being FinSequence of D st
( x = p & len p = n ) )
assume A2: x in rng s ; :: thesis: ex p being FinSequence of D st
( x = p & len p = n )
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: ( x = p & len p = n )
thus ( x = p & len p = n ) by A3, A4; :: thesis: verum

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: verum

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: s is Matrix of D
A6: s is tabular

proof

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 s being FinSequence st
( s = x & len s = n )
for x being object st x in rng s holds
ex t being FinSequence st
( t = x & len t = n )

proof

let x be object ; :: thesis: ( x in rng s implies ex t being FinSequence st
( t = x & len t = n ) )
assume x in rng s ; :: thesis: ex t being FinSequence st
( t = x & len t = n )
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: ( t = x & len t = n )
thus ( t = x & len t = n ) by A8; :: thesis: verum

end;

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

end;

rng s c= D *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s or x in D * )
assume x in rng s ; :: thesis: x in D *
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: verum

end;

hence s is Matrix of D by A6, FINSEQ_1:def 4; :: thesis: verum