let i, j be 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 A1: [i,j] in Indices M ; :: thesis: ( i in dom M & j in dom (M . i) )
then A2: j in Seg (width M) by Th12;
A3: i in Seg (len M) by A1, Th12;
then i in dom M by FINSEQ_1:def 3;
then j in Seg (len (M . i)) by A2, MATRIX_0:36;
hence ( i in dom M & j in dom (M . i) ) by A3, 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 MATRIX_0:37; :: thesis: verum