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 i in dom (n,m --> a) by ZFMISC_1:106;
then i in Seg (len (n,m --> a)) by FINSEQ_1:def 3;
then A2: i in Seg n by MATRIX_1:def 3;
then A3: n > 0 ;
j in Seg (width (n,m --> a)) by A1, ZFMISC_1:106;
then j in Seg m by A3, MATRIX_1:24;
then A4: (m1 |-> a) . j = a by FUNCOP_1:13;
(n,m --> a) . i = m1 |-> a by A2, FUNCOP_1:13;
hence (n,m --> a) * i,j = a by A1, A4, MATRIX_1:def 6; :: thesis: verum