theorem :: FINSEQ_2:118

for i being natural Number
for D being non empty set
for z being Tuple of i,D holds z * (idseq i) = z