let i be Nat; :: thesis: for D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
let D be non empty set ; :: thesis: for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
let f be FinSequence of D; :: thesis: for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
let M be Matrix of D; :: thesis: ( i in dom M & M . i = f implies len f = width M )
assume that
A1: i in dom M and
A2: M . i = f ; :: thesis: len f = width M
not M is empty by A1;
then len M > 0 ;
then consider p being FinSequence such that
A3: p in rng M and
A4: len p = width M by Def3;
consider n being Nat such that
A5: for x being object st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
M . i in rng M by A1, FUNCT_1:def 3;
then A6: ex s being FinSequence st
( s = M . i & len s = n ) by A5;
ex s being FinSequence st
( s = p & len s = n ) by A3, A5;
hence len f = width M by A2, A4, A6; :: thesis: verum