let D, E be non empty set ; for n, m, i, j being Nat
for M being Matrix of n,m,D st 0 < n & M is Matrix of n,m,E & [i,j] in Indices M holds
M * (i,j) is Element of E
let n, m, i, j be Nat; for M being Matrix of n,m,D st 0 < n & M is Matrix of n,m,E & [i,j] in Indices M holds
M * (i,j) is Element of E
let M be Matrix of n,m,D; ( 0 < n & M is Matrix of n,m,E & [i,j] in Indices M implies M * (i,j) is Element of E )
assume that
A1:
0 < n
and
A2:
M is Matrix of n,m,E
and
A3:
[i,j] in Indices M
; M * (i,j) is Element of E
consider m1 being Nat such that
A4:
for x being object st x in rng M holds
ex q being FinSequence of E st
( x = q & len q = m1 )
by MATRIX_0:9, A2;
consider p being FinSequence of D such that
A5:
( p = M . i & M * (i,j) = p . j )
by A3, MATRIX_0:def 5;
A6:
( i in dom M & j in Seg (width M) )
by A3, ZFMISC_1:87;
then A7:
p in rng M
by FUNCT_1:3, A5;
ex q being FinSequence of E st
( p = q & len q = m1 )
by A4, A5, A6, FUNCT_1:3;
then A50:
rng p c= E
by FINSEQ_1:def 4;
len p = m
by A7, MATRIX_0:def 2;
then
len p = width M
by A1, MATRIX_0:23;
then
j in dom p
by FINSEQ_1:def 3, A6;
hence
M * (i,j) is Element of E
by A5, A50, FUNCT_1:3; verum