theorem LMGSEQ4: :: AESCIP_1:8

for D being non empty set
for x1, x2, x3, x4 being Element of D holds <*x1,x2,x3,x4*> is Element of 4 -tuples_on D