let i, j be Element of NAT ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( [i,j] in Indices M & M . i = f implies ( len f = width M & j in dom f ) )
assume A1: [i,j] in Indices M ; :: thesis: ( not M . i = f or ( len f = width M & j in dom f ) )
A2: Indices M = [:(dom M),(Seg (width M)):] by MATRIX_1:def 4;
then A3: j in Seg (width M) by A1, ZFMISC_1:87;
not M is empty by A1, A2, ZFMISC_1:87;
then len M > 0 by NAT_1:3;
then consider p being FinSequence such that
A4: p in rng M and
A5: len p = width M by MATRIX_1:def 3;
consider n being Nat such that
A6: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by MATRIX_1:def 1;
i in dom M by A1, A2, ZFMISC_1:87;
then M . i in rng M by FUNCT_1:def 3;
then A7: ex s being FinSequence st
( s = M . i & len s = n ) by A6;
ex s being FinSequence st
( s = p & len s = n ) by A4, A6;
hence ( not M . i = f or ( len f = width M & j in dom f ) ) by A3, A5, A7, FINSEQ_1:def 3; :: thesis: verum