theorem Th5: :: NUMBER17:5
for D being non empty set holds 5 -tuples_on D = { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum }