let C1, C2 be Coherence_Space; :: thesis: for x, y being set holds
( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) )
let x, y be set ; :: thesis: ( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) )

now

given a being Element of C1, b being Element of C2 such that A1: x U+ y = a U+ b ; :: thesis: ex a being Element of C1 ex b being Element of C2 st
( x = a & y = b )
take a = a; :: thesis: ex b being Element of C2 st
( x = a & y = b )
take b = b; :: thesis: ( x = a & y = b )
thus ( x = a & y = b ) by A1, Th81; :: thesis: verum

end;

hence ( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) ) ; :: thesis: verum