let i be Nat; :: thesis: for D being non empty set
for z being Element of i -tuples_on D holds z * (idseq i) = z
let D be non empty set ; :: thesis: for z being Element of i -tuples_on D holds z * (idseq i) = z
let z be Element of i -tuples_on D; :: thesis: z * (idseq i) = z
len z = i by FINSEQ_1:def 18;
hence z * (idseq i) = z by Th64; :: thesis: verum