let C1, C2 be Coherence_Space; :: thesis: union (C1 [*] C2) = [:(union C1),(union C2):]
thus union (C1 [*] C2) c= [:(union C1),(union C2):] :: according to XBOOLE_0:def 10 :: thesis: [:(union C1),(union C2):] c= union (C1 [*] C2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (C1 [*] C2) or x in [:(union C1),(union C2):] )
assume x in union (C1 [*] C2) ; :: thesis: x in [:(union C1),(union C2):]
then consider a being set such that
A1: ( x in a & a in C1 [*] C2 ) by TARSKI:def 4;
consider a1 being Element of C1, a2 being Element of C2 such that
A2: a c= [:a1,a2:] by A1, Th97;
( a1 c= union C1 & a2 c= union C2 ) by ZFMISC_1:92;
then [:a1,a2:] c= [:(union C1),(union C2):] by ZFMISC_1:119;
then a c= [:(union C1),(union C2):] by A2, XBOOLE_1:1;
hence x in [:(union C1),(union C2):] by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(union C1),(union C2):] or x in union (C1 [*] C2) )
assume x in [:(union C1),(union C2):] ; :: thesis: x in union (C1 [*] C2)
then A3: ( x = [(x `1 ),(x `2 )] & x `1 in union C1 & x `2 in union C2 ) by MCART_1:10, MCART_1:23;
then consider a1 being set such that
A4: ( x `1 in a1 & a1 in C1 ) by TARSKI:def 4;
consider a2 being set such that
A5: ( x `2 in a2 & a2 in C2 ) by A3, TARSKI:def 4;
( x in [:a1,a2:] & [:a1,a2:] in C1 [*] C2 ) by A3, A4, A5, Th97, ZFMISC_1:106;
hence x in union (C1 [*] C2) by TARSKI:def 4; :: thesis: verum