theorem Th18: :: NAGATA_2:18

for D being non empty set
for p, q being FinSequence of D
for B being BinOp of D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )