theorem Th19: :: COH_SP:19

for X being set
for C1, C2 being Element of CSp X
for f being Function of (union C1),(union C2) st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds
{(f . x),(f . y)} in C2 ) holds
[[C1,C2],f] in MapsC X