theorem :: COHSP_1:47

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