let i, j, n, m be Nat; :: thesis: for D being non empty set
for a being Element of D st [i,j] in Indices (n,m --> a) holds
(n,m --> a) * i,j = a
let D be non empty set ; :: thesis: for a being Element of D st [i,j] in Indices (n,m --> a) holds
(n,m --> a) * i,j = a
let a be Element of D; :: thesis: ( [i,j] in Indices (n,m --> a) implies (n,m --> a) * i,j = a )
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
set M = n,m --> a;
assume A1: [i,j] in Indices (n,m --> a) ; :: thesis: (n,m --> a) * i,j = a
then A2: ( i in dom (n,m --> a) & j in Seg (width (n,m --> a)) ) by ZFMISC_1:106;
then i in Seg (len (n,m --> a)) by FINSEQ_1:def 3;
then A3: i in Seg n by MATRIX_1:def 3;
then n > 0 by FINSEQ_1:4;
then j in Seg m by A2, MATRIX_1:24;
then ( (n,m --> a) . i = m1 |-> a & (m1 |-> a) . j = a ) by A3, FUNCOP_1:13;
hence (n,m --> a) * i,j = a by A1, MATRIX_1:def 6; :: thesis: verum