let D be non empty set ; :: thesis: for d being Element of D holds <*d*> /. 1 = d
let d be Element of D; :: thesis: <*d*> /. 1 = d
( dom <*d*> = {1} & <*d*> . 1 = d & 1 in {1} ) by FINSEQ_1:4, FINSEQ_1:def 8;
hence <*d*> /. 1 = d by PARTFUN1:def 8; :: thesis: verum