let X1, X2, Y be set ; :: thesis: (X1 \/ X2) ++ Y = (X1 ++ Y) \/ (X2 ++ Y)
thus (X1 \/ X2) ++ Y c= (X1 ++ Y) \/ (X2 ++ Y) :: according to XBOOLE_0:def 10 :: thesis: (X1 ++ Y) \/ (X2 ++ Y) c= (X1 \/ X2) ++ Y

proof

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in (X1 \/ X2) ++ Y or xy in (X1 ++ Y) \/ (X2 ++ Y) )
assume xy in (X1 \/ X2) ++ Y ; :: thesis: xy in (X1 ++ Y) \/ (X2 ++ Y)
then consider x, y being Surreal such that
A1: ( x in X1 \/ X2 & y in Y & xy = x + y ) by Def8;
( x in X1 or x in X2 ) by A1, XBOOLE_0:def 3;
then ( xy in X1 ++ Y or xy in X2 ++ Y ) by A1, Def8;
hence xy in (X1 ++ Y) \/ (X2 ++ Y) by XBOOLE_0:def 3; :: thesis: verum

end;

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in (X1 ++ Y) \/ (X2 ++ Y) or xy in (X1 \/ X2) ++ Y )
assume xy in (X1 ++ Y) \/ (X2 ++ Y) ; :: thesis: xy in (X1 \/ X2) ++ Y

per cases then ( xy in X1 ++ Y or xy in X2 ++ Y ) by XBOOLE_0:def 3;

suppose xy in X1 ++ Y ; :: thesis: xy in (X1 \/ X2) ++ Y

then consider x, y being Surreal such that
A2: ( x in X1 & y in Y & xy = x + y ) by Def8;
x in X1 \/ X2 by A2, XBOOLE_0:def 3;
hence xy in (X1 \/ X2) ++ Y by A2, Def8; :: thesis: verum

end;

suppose xy in X2 ++ Y ; :: thesis: xy in (X1 \/ X2) ++ Y

then consider x, y being Surreal such that
A3: ( x in X2 & y in Y & xy = x + y ) by Def8;
x in X1 \/ X2 by A3, XBOOLE_0:def 3;
hence xy in (X1 \/ X2) ++ Y by A3, Def8; :: thesis: verum

end;

end;