let D, E be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum