for X being non empty disjoint_with_NAT set
for I1, I2, J1, J2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st I1 \; I2 = J1 \; J2 holds
( I1 = J1 & I2 = J2 )