let i, j be Nat; for D being non empty set
for f being FinSequence of D
for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
let D be non empty set ; for f being FinSequence of D
for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
let f be FinSequence of D; for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
let M be Matrix of D; ( [i,j] in Indices M & M . i = f implies ( len f = width M & j in dom f ) )
assume A1:
[i,j] in Indices M
; ( not M . i = f or ( len f = width M & j in dom f ) )
A2:
j in Seg (width M)
by A1, ZFMISC_1:87;
not M is empty
by A1, ZFMISC_1:87;
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;
i in dom M
by A1, ZFMISC_1:87;
then
M . i in rng M
by 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
( not M . i = f or ( len f = width M & j in dom f ) )
by A2, A4, A6, FINSEQ_1:def 3; verum