let D be set ; :: thesis: for d being Element of D holds (Seg 1) --> d = <*d*>
let d be Element of D; :: thesis: (Seg 1) --> d = <*d*>
(Seg 1) --> d = 1 |-> d
.= <*d*> by FINSEQ_2:59 ;
hence (Seg 1) --> d = <*d*> ; :: thesis: verum