let D be set ; :: thesis: for z being FinSequence of D holds z is Element of (len z) -tuples_on D
let z be FinSequence of D; :: thesis: z is Element of (len z) -tuples_on D
z is Element of D * by FINSEQ_1:def 11;
then z in { z9 where z9 is Element of D * : len z9 = len z } ;
hence z is Element of (len z) -tuples_on D ; :: thesis: verum