let i be natural Number ; :: thesis: for D being non empty set
for z being Tuple of i,D holds z * (idseq i) = z
let D be non empty set ; :: thesis: for z being Tuple of i,D holds z * (idseq i) = z
let z be Tuple of i,D; :: thesis: z * (idseq i) = z
len z = i by CARD_1:def 7;
hence z * (idseq i) = z by Th52; :: thesis: verum