let z be Element of i -tuples_on D; :: thesis: z is i -element
z in { p9 where p9 is Element of D * : len p9 = i } ;
then ex p9 being Element of D * st
( p9 = z & len p9 = i ) ;
hence len z = i ; :: according to CARD_1:def 7 :: thesis: verum