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 (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_0:def 8;
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_0:60; :: 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_0:def 8;
then A5: i in dom M by FINSEQ_1:def 3;
then j in dom (M . i) by A4, MATRIX_0:60;
hence [i,j] in Indices M by A5, Th13; :: thesis: verum