let x, y be Surreal; :: thesis: for X, Y1, Y2 being set holds comp (X,x,y,(Y1 \/ Y2)) = (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2))
let X, Y1, Y2 be set ; :: thesis: comp (X,x,y,(Y1 \/ Y2)) = (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2))
thus comp (X,x,y,(Y1 \/ Y2)) c= (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2)) :: according to XBOOLE_0:def 10 :: thesis: (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2)) c= comp (X,x,y,(Y1 \/ Y2))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in comp (X,x,y,(Y1 \/ Y2)) or o in (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2)) )
assume o in comp (X,x,y,(Y1 \/ Y2)) ; :: thesis: o in (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2))
then consider x1, y1 being Surreal such that
A1: ( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y1 \/ Y2 ) by Def14;
( y1 in Y1 or y1 in Y2 ) by A1, XBOOLE_0:def 3;
then ( o in comp (X,x,y,Y1) or o in comp (X,x,y,Y2) ) by A1, Def14;
hence o in (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2)) by XBOOLE_0:def 3; :: thesis: verum

end;

( comp (X,x,y,Y1) c= comp (X,x,y,(Y1 \/ Y2)) & comp (X,x,y,Y2) c= comp (X,x,y,(Y1 \/ Y2)) ) by XBOOLE_1:7, Th59;
hence (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2)) c= comp (X,x,y,(Y1 \/ Y2)) by XBOOLE_1:8; :: thesis: verum