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