theorem :: FINSEQ_2:103

for D being non empty set
for z being Tuple of 3,D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>