let x1, y1, x2, y2 be set ; (x1 U+ y1) \/ (x2 U+ y2) = (x1 \/ x2) U+ (y1 \/ y2)
set X1 = [:x1,{1}:];
set X2 = [:x2,{1}:];
set Y1 = [:y1,{2}:];
set Y2 = [:y2,{2}:];
set X = [:(x1 \/ x2),{1}:];
set Y = [:(y1 \/ y2),{2}:];
A1:
[:(x1 \/ x2),{1}:] = [:x1,{1}:] \/ [:x2,{1}:]
by ZFMISC_1:97;
A2:
( (x1 \/ x2) U+ (y1 \/ y2) = [:(x1 \/ x2),{1}:] \/ [:(y1 \/ y2),{2}:] & [:(y1 \/ y2),{2}:] = [:y1,{2}:] \/ [:y2,{2}:] )
by Th73, ZFMISC_1:97;
( x1 U+ y1 = [:x1,{1}:] \/ [:y1,{2}:] & x2 U+ y2 = [:x2,{1}:] \/ [:y2,{2}:] )
by Th73;
hence (x1 U+ y1) \/ (x2 U+ y2) =
(([:x1,{1}:] \/ [:y1,{2}:]) \/ [:x2,{1}:]) \/ [:y2,{2}:]
by XBOOLE_1:4
.=
([:(x1 \/ x2),{1}:] \/ [:y1,{2}:]) \/ [:y2,{2}:]
by A1, XBOOLE_1:4
.=
(x1 \/ x2) U+ (y1 \/ y2)
by A2, XBOOLE_1:4
;
verum