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
A1: 1 in {1} by FINSEQ_1:2;
( dom <*d*> = {1} & <*d*> . 1 = d ) by FINSEQ_1:2, FINSEQ_1:def 8;
hence <*d*> /. 1 = d by A1, PARTFUN1:def 6; :: thesis: verum