let X, Y, Z be set ; :: thesis: ( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )
A1: for z, X1, X2, Y1, Y2 being set st z in [:X1,X2:] \/ [:Y1,Y2:] holds
ex x, y being set st z = [x,y]

proof

let z, X1, X2, Y1, Y2 be set ; :: thesis: ( z in [:X1,X2:] \/ [:Y1,Y2:] implies ex x, y being set st z = [x,y] )
assume z in [:X1,X2:] \/ [:Y1,Y2:] ; :: thesis: ex x, y being set st z = [x,y]
then ( z in [:X1,X2:] or z in [:Y1,Y2:] ) by XBOOLE_0:def 3;
hence ex x, y being set st z = [x,y] by Lm20; :: thesis: verum

end;

thus A2: [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] :: thesis: [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:]

proof

A3: ( ( for z being set st z in [:X,Z:] \/ [:Y,Z:] holds
ex x, y being set st z = [x,y] ) & ( for z being set st z in [:(X \/ Y),Z:] holds
ex x, y being set st z = [x,y] ) ) by A1, Lm20;
for x, y being set holds
( [x,y] in [:(X \/ Y),Z:] iff [x,y] in [:X,Z:] \/ [:Y,Z:] )

proof

let x, y be set ; :: thesis: ( [x,y] in [:(X \/ Y),Z:] iff [x,y] in [:X,Z:] \/ [:Y,Z:] )
thus ( [x,y] in [:(X \/ Y),Z:] implies [x,y] in [:X,Z:] \/ [:Y,Z:] ) :: thesis: ( [x,y] in [:X,Z:] \/ [:Y,Z:] implies [x,y] in [:(X \/ Y),Z:] )

proof

assume [x,y] in [:(X \/ Y),Z:] ; :: thesis: [x,y] in [:X,Z:] \/ [:Y,Z:]
then ( x in X \/ Y & y in Z ) by Lm17;
then ( ( x in X or x in Y ) & y in Z ) by XBOOLE_0:def 3;
then ( [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) by Lm17;
hence [x,y] in [:X,Z:] \/ [:Y,Z:] by XBOOLE_0:def 3; :: thesis: verum

end;

assume [x,y] in [:X,Z:] \/ [:Y,Z:] ; :: thesis: [x,y] in [:(X \/ Y),Z:]
then ( [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) by XBOOLE_0:def 3;
then ( ( x in X & y in Z ) or ( x in Y & y in Z ) ) by Lm17;
then ( x in X \/ Y & y in Z ) by XBOOLE_0:def 3;
hence [x,y] in [:(X \/ Y),Z:] by Lm17; :: thesis: verum

end;

hence [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] by A3, Lm19; :: thesis: verum

end;

A4: ( ( for z being set st z in [:Z,X:] \/ [:Z,Y:] holds
ex x, y being set st z = [x,y] ) & ( for z being set st z in [:Z,(X \/ Y):] holds
ex x, y being set st z = [x,y] ) ) by A1, Lm20;
for y, x being set holds
( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] )

proof

let y, x be set ; :: thesis: ( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] )
( ( [y,x] in [:Z,(X \/ Y):] implies [x,y] in [:(X \/ Y),Z:] ) & ( [x,y] in [:(X \/ Y),Z:] implies [y,x] in [:Z,(X \/ Y):] ) & ( not [x,y] in [:X,Z:] \/ [:Y,Z:] or [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) & ( ( [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) implies [x,y] in [:X,Z:] \/ [:Y,Z:] ) & ( ( not [x,y] in [:X,Z:] & not [x,y] in [:Y,Z:] ) or [y,x] in [:Z,X:] or [y,x] in [:Z,Y:] ) & ( ( not [y,x] in [:Z,X:] & not [y,x] in [:Z,Y:] ) or [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) ) by Th107, XBOOLE_0:def 3;
hence ( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] ) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

hence [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] by A4, Lm19; :: thesis: verum