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 Nat ;
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:87;
then i in Seg (len ((n,m) --> a)) by FINSEQ_1:def 3;
then A2: i in Seg n by Def2;
then A3: n > 0 ;
j in Seg (width ((n,m) --> a)) by A1, ZFMISC_1:87;
then j in Seg m by A3, Th23;
then A4: (m1 |-> a) . j = a by FUNCOP_1:7;
((n,m) --> a) . i = m1 |-> a by A2, FUNCOP_1:7;
hence ((n,m) --> a) * (i,j) = a by A1, A4, Def5; :: thesis: verum