let D be non empty set ; :: thesis: for i0, j0, n0, m0 being non zero Nat
for A being Matrix of D st i0 < j0 & n0 < m0 holds
Segm A,{i0,j0},{n0,m0} = (A * i0,n0),(A * i0,m0) ][ (A * j0,n0),(A * j0,m0)
let i0, j0, n0, m0 be non zero Nat; :: thesis: for A being Matrix of D st i0 < j0 & n0 < m0 holds
Segm A,{i0,j0},{n0,m0} = (A * i0,n0),(A * i0,m0) ][ (A * j0,n0),(A * j0,m0)
let A be Matrix of D; :: thesis: ( i0 < j0 & n0 < m0 implies Segm A,{i0,j0},{n0,m0} = (A * i0,n0),(A * i0,m0) ][ (A * j0,n0),(A * j0,m0) )
assume that
A1: i0 < j0 and
A2: n0 < m0 ; :: thesis: Segm A,{i0,j0},{n0,m0} = (A * i0,n0),(A * i0,m0) ][ (A * j0,n0),(A * j0,m0)
A3: card {n0,m0} = 2 by A2, CARD_2:76;
A4: Sgm {n0,m0} = <*n0,m0*> by A2, FINSEQ_3:51;
then A5: (Sgm {n0,m0}) . 1 = n0 by FINSEQ_1:61;
A6: Sgm {i0,j0} = <*i0,j0*> by A1, FINSEQ_3:51;
then A7: (Sgm {i0,j0}) . 1 = i0 by FINSEQ_1:61;
A8: (Sgm {i0,j0}) . 2 = j0 by A6, FINSEQ_1:61;
A9: (Sgm {n0,m0}) . 2 = m0 by A4, FINSEQ_1:61;
card {i0,j0} = 2 by A1, CARD_2:76;
hence Segm A,{i0,j0},{n0,m0} = (A * i0,n0),(A * i0,m0) ][ (A * j0,n0),(A * j0,m0) by A3, A5, A9, A7, A8, Th23; :: thesis: verum