let D be non empty set ; for n, m being Nat
for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
let n, m be Nat; for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
let e1 be FinSequence of D; ( len e1 = m implies n |-> e1 is Matrix of n,m,D )
assume A1:
len e1 = m
; n |-> e1 is Matrix of n,m,D
reconsider e = n |-> e1 as FinSequence of D * by Th8;
A2:
len e = n
by CARD_1:def 7;
A3:
for i being Nat st i in dom e holds
len (e . i) = m
then reconsider e = e as Matrix of D by Th11;
for p being FinSequence of D st p in rng e holds
len p = m
hence
n |-> e1 is Matrix of n,m,D
by A2, MATRIX_0:def 2; verum