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 (Col M,j) & j in dom (Line 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 (Col M,j) & j in dom (Line M,i) ) )
let M be Matrix of D; :: thesis: ( [i,j] in Indices M iff ( i in dom (Col M,j) & j in dom (Line M,i) ) )

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

assume [i,j] in Indices M ; :: thesis: ( i in dom (Col M,j) & j in dom (Line M,i) )
then A1: ( i in dom M & j in dom (M . i) ) by Th13;
then i in Seg (len M) by FINSEQ_1:def 3;
then i in Seg (len (Col M,j)) by MATRIX_1:def 9;
hence i in dom (Col M,j) by FINSEQ_1:def 3; :: thesis: j in dom (Line M,i)
thus j in dom (Line M,i) by A1, MATRIX_2:18; :: thesis: verum

end;

assume A2: ( i in dom (Col M,j) & j in dom (Line M,i) ) ; :: thesis: [i,j] in Indices M
then i in Seg (len (Col M,j)) by FINSEQ_1:def 3;
then i in Seg (len M) by MATRIX_1:def 9;
then A3: i in dom M by FINSEQ_1:def 3;
then j in dom (M . i) by A2, MATRIX_2:18;
hence [i,j] in Indices M by A3, Th13; :: thesis: verum