theorem :: FINSEQ_4:16

for D being non empty set
for d being Element of D holds <*d*> /. 1 = d