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)*>*>
A1: card {j0} = 1 by CARD_1:50;
A2: Sgm {i0} = <*i0*> by FINSEQ_3:50;
A3: <*j0*> . 1 = j0 by FINSEQ_1:57;
A4: <*i0*> . 1 = i0 by FINSEQ_1:57;
A5: Sgm {j0} = <*j0*> by FINSEQ_3:50;
card {i0} = 1 by CARD_1:50;
hence Segm A,{i0},{j0} = <*<*(A * i0,j0)*>*> by A1, A2, A5, A4, A3, Th21; :: thesis: verum