theorem Th4: :: NORMSP_4:4

for X being addLoopStr
for A, B being Subset of X ex F being Function of (A + B),[:A,B:] st F is one-to-one