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:57;
A4: Sgm {n0,m0} = <*n0,m0*> by A2, FINSEQ_3:45;
then A5: (Sgm {n0,m0}) . 1 = n0 by FINSEQ_1:44;
A6: Sgm {i0,j0} = <*i0,j0*> by A1, FINSEQ_3:45;
then A7: (Sgm {i0,j0}) . 1 = i0 by FINSEQ_1:44;
A8: (Sgm {i0,j0}) . 2 = j0 by A6, FINSEQ_1:44;
A9: (Sgm {n0,m0}) . 2 = m0 by A4, FINSEQ_1:44;
card {i0,j0} = 2 by A1, CARD_2:57;
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