theorem Th3: :: DESCIP_1:3

for D being non empty set
for n being non zero Element of NAT
for s being Element of (2 * n) -tuples_on D holds (SP-Left s) ^ (SP-Right s) = s by RFINSEQ:8;