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 A1: [i,j] in Indices M ; :: thesis: ( i in dom (Col M,j) & j in dom (Line M,i) )
then A2: i in dom M 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)
j in dom (M . i) by A1, Th13;
hence j in dom (Line M,i) by A2, MATRIX_2:18; :: thesis: verum

end;

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