let i, j be Element of NAT ; :: thesis: for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )
let D be non empty set ; :: thesis: for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )
let M be Matrix of D; :: thesis: ( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )

hereby :: thesis: ( i in dom M & j in dom (M . i) implies [i,j] in Indices M )

assume [i,j] in Indices M ; :: thesis: ( i in dom M & j in dom (M . i) )
then A1: ( i in Seg (len M) & j in Seg (width M) ) by Th12;
then i in dom M by FINSEQ_1:def 3;
then j in Seg (len (M . i)) by A1, GOBRD13:4;
hence ( i in dom M & j in dom (M . i) ) by A1, FINSEQ_1:def 3; :: thesis: verum

end;

assume ( i in dom M & j in dom (M . i) ) ; :: thesis: [i,j] in Indices M
hence [i,j] in Indices M by GOBRD13:5; :: thesis: verum