let z be Element of i -tuples_on D; :: thesis: z is i -long
z in { p' where p' is Element of D * : len p' = i } ;
then ex p' being Element of D * st
( p' = z & len p' = i ) ;
hence len z = i ; :: according to FINSEQ_1:def 18 :: thesis: verum