let D be non empty set ; :: thesis: for z being Tuple of 2,D ex d1, d2 being Element of D st z = <*d1,d2*>
let z be Tuple of 2,D; :: thesis: ex d1, d2 being Element of D st z = <*d1,d2*>
A: z is Element of D * by FINSEQ_1:def 11;
len z = 2 by FINSEQ_1:def 18;
then z in 2 -tuples_on D by A;
then z in { <*d1,d2*> where d1, d2 is Element of D : verum } by Th119;
hence ex d1, d2 being Element of D st z = <*d1,d2*> ; :: thesis: verum