theorem :: FINSEQ_4:17

for D being non empty set
for d1, d2 being Element of D holds
( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 )