let D be non empty set ; :: thesis: for i0, j0 being non zero Nat
for A being Matrix of D holds Segm A,{i0},{j0} = <*<*(A * i0,j0)*>*>
let i0, j0 be non zero Nat; :: thesis: for A being Matrix of D holds Segm A,{i0},{j0} = <*<*(A * i0,j0)*>*>
let A be Matrix of D; :: thesis: Segm A,{i0},{j0} = <*<*(A * i0,j0)*>*>
( card {i0} = 1 & card {j0} = 1 & Sgm {i0} = <*i0*> & Sgm {j0} = <*j0*> & <*i0*> . 1 = i0 & <*j0*> . 1 = j0 ) by CARD_1:50, FINSEQ_1:57, FINSEQ_3:50;
hence Segm A,{i0},{j0} = <*<*(A * i0,j0)*>*> by Th21; :: thesis: verum