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 ( i0 < j0 & n0 < m0 ) ; :: thesis: Segm A,{i0,j0},{n0,m0} = (A * i0,n0),(A * i0,m0) ][ (A * j0,n0),(A * j0,m0)
then A1: ( card {i0,j0} = 2 & card {n0,m0} = 2 & Sgm {i0,j0} = <*i0,j0*> & Sgm {n0,m0} = <*n0,m0*> ) by CARD_2:76, FINSEQ_3:51;
then ( (Sgm {n0,m0}) . 1 = n0 & (Sgm {n0,m0}) . 2 = m0 & (Sgm {i0,j0}) . 1 = i0 & (Sgm {i0,j0}) . 2 = j0 ) by FINSEQ_1:61;
hence Segm A,{i0,j0},{n0,m0} = (A * i0,n0),(A * i0,m0) ][ (A * j0,n0),(A * j0,m0) by A1, Th23; :: thesis: verum