theorem :: COHSP_1:63

for C1, C2 being Coherence_Space holds union (LinCoh (C1,C2)) = [:(union C1),(union C2):]