let D be non empty set ; :: thesis: for z being Tuple of 5,D ex d1, d2, d3, d4, d5 being Element of D st z = <*d1,d2,d3,d4,d5*>
let z be Tuple of 5,D; :: thesis: ex d1, d2, d3, d4, d5 being Element of D st z = <*d1,d2,d3,d4,d5*>
A1: z is Element of D * by FINSEQ_1:def 11;
len z = 5 by CARD_1:def 7;
then z in 5 -tuples_on D by A1;
then z in { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum } by Th5;
hence ex d1, d2, d3, d4, d5 being Element of D st z = <*d1,d2,d3,d4,d5*> ; :: thesis: verum