theorem :: AESCIP_1:13

for D being non empty set
for x being Element of 4 -tuples_on (4 -tuples_on D)
for k being Element of NAT st k in Seg 4 holds
ex x1, x2, x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )