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