let D be non empty set ; 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; ex d1, d2 being Element of D st z = <*d1,d2*>
A1:
z is Element of D *
by FINSEQ_1:def 11;
len z = 2
by CARD_1:def 7;
then
z in 2 -tuples_on D
by A1;
then
z in { <*d1,d2*> where d1, d2 is Element of D : verum }
by Th97;
hence
ex d1, d2 being Element of D st z = <*d1,d2*>
; verum