let i be Nat; :: 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 FINSEQ_1:def 18;
hence z * (idseq i) = z by Th64; :: thesis: verum