let D be set ; :: thesis: for e being FinSequence of D * holds
( ex n being Nat st
for i being Nat st i in dom e holds
len (e . i) = n iff e is Matrix of D )
let e be FinSequence of D * ; :: thesis: ( ex n being Nat st
for i being Nat st i in dom e holds
len (e . i) = n iff e is Matrix of D )

hereby :: thesis: ( e is Matrix of D implies ex n being Nat st
for i being Nat st i in dom e holds
len (e . i) = n )

given n being Nat such that A1: for i being Nat st i in dom e holds
len (e . i) = n ; :: thesis: e is Matrix of D
for i being Nat st i in dom e holds
ex p being FinSequence of D st
( e . i = p & len p = n )

proof

let i be Nat; :: thesis: ( i in dom e implies ex p being FinSequence of D st
( e . i = p & len p = n ) )
assume i in dom e ; :: thesis: ex p being FinSequence of D st
( e . i = p & len p = n )
then len (e . i) = n by A1;
hence ex p being FinSequence of D st
( e . i = p & len p = n ) ; :: thesis: verum

end;

hence e is Matrix of D by Th10; :: thesis: verum

end;

assume e is Matrix of D ; :: thesis: ex n being Nat st
for i being Nat st i in dom e holds
len (e . i) = n
then consider n being Nat such that
A2: for i being Nat st i in dom e holds
ex p being FinSequence of D st
( e . i = p & len p = n ) by Th10;
for i being Nat st i in dom e holds
len (e . i) = n

proof

let i be Nat; :: thesis: ( i in dom e implies len (e . i) = n )
assume i in dom e ; :: thesis: len (e . i) = n
then ex p being FinSequence of D st
( e . i = p & len p = n ) by A2;
hence len (e . i) = n ; :: thesis: verum

end;

hence ex n being Nat st
for i being Nat st i in dom e holds
len (e . i) = n ; :: thesis: verum