let x1, y1, x2, y2 be set ; :: thesis: (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 ;
:: thesis: verum