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:99;
A2: {1} misses {2} by ZFMISC_1:11;
then [:y1,{2}:] misses [:x2,{1}:] by ZFMISC_1:104;
then A3: ( [:(y1 /\ y2),{2}:] = [:y1,{2}:] /\ [:y2,{2}:] & [:y1,{2}:] /\ [:x2,{1}:] = {} ) by ZFMISC_1:99;
[:x1,{1}:] misses [:y2,{2}:] by A2, ZFMISC_1:104;
then A4: [:x1,{1}:] /\ [:y2,{2}:] = {} ;
( 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}:]) \/ (([:x1,{1}:] \/ [:y1,{2}:]) /\ [:y2,{2}:]) by XBOOLE_1:23
.= ([:(x1 /\ x2),{1}:] \/ ([:y1,{2}:] /\ [:x2,{1}:])) \/ (([:x1,{1}:] \/ [:y1,{2}:]) /\ [:y2,{2}:]) by A1, XBOOLE_1:23
.= [:(x1 /\ x2),{1}:] \/ (([:x1,{1}:] /\ [:y2,{2}:]) \/ [:(y1 /\ y2),{2}:]) by A3, XBOOLE_1:23
.= (x1 /\ x2) U+ (y1 /\ y2) by A4, Th73 ;
:: thesis: verum