let X, Y, Z be set ; ( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )
A1:
for z being object st z in [:(X \/ Y),Z:] holds
ex x, y being object st z = [x,y]
by Lm19;
A2:
for x, y being object holds
( [x,y] in [:(X \/ Y),Z:] iff [x,y] in [:X,Z:] \/ [:Y,Z:] )
proof
let x,
y be
object ;
( [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:] )
( [x,y] in [:X,Z:] \/ [:Y,Z:] implies [x,y] in [:(X \/ Y),Z:] )proof
assume A3:
[x,y] in [:(X \/ Y),Z:]
;
[x,y] in [:X,Z:] \/ [:Y,Z:]
then
x in X \/ Y
by Lm16;
then A4:
(
x in X or
x in Y )
by XBOOLE_0:def 3;
y in Z
by A3, Lm16;
then
(
[x,y] in [:X,Z:] or
[x,y] in [:Y,Z:] )
by A4, Lm16;
hence
[x,y] in [:X,Z:] \/ [:Y,Z:]
by XBOOLE_0:def 3;
verum
end;
assume
[x,y] in [:X,Z:] \/ [:Y,Z:]
;
[x,y] in [:(X \/ Y),Z:]
then
(
[x,y] in [:X,Z:] or
[x,y] in [:Y,Z:] )
by XBOOLE_0:def 3;
then A5:
( (
x in X &
y in Z ) or (
x in Y &
y in Z ) )
by Lm16;
then
x in X \/ Y
by XBOOLE_0:def 3;
hence
[x,y] in [:(X \/ Y),Z:]
by A5, Lm16;
verum
end;
A6:
for z being object
for X1, X2, Y1, Y2 being set st z in [:X1,X2:] \/ [:Y1,Y2:] holds
ex x, y being object st z = [x,y]
proof
let z be
object ;
for X1, X2, Y1, Y2 being set st z in [:X1,X2:] \/ [:Y1,Y2:] holds
ex x, y being object st z = [x,y]let X1,
X2,
Y1,
Y2 be
set ;
( z in [:X1,X2:] \/ [:Y1,Y2:] implies ex x, y being object st z = [x,y] )
assume
z in [:X1,X2:] \/ [:Y1,Y2:]
;
ex x, y being object st z = [x,y]
then
(
z in [:X1,X2:] or
z in [:Y1,Y2:] )
by XBOOLE_0:def 3;
hence
ex
x,
y being
object st
z = [x,y]
by Lm19;
verum
end;
then
for z being object st z in [:X,Z:] \/ [:Y,Z:] holds
ex x, y being object st z = [x,y]
;
hence A7:
[:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:]
by A1, A2, Lm18; [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:]
A8:
for y, x being object holds
( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] )
proof
let y,
x be
object ;
( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] )
A9:
( ( ( 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 Th87;
(
[y,x] in [:Z,(X \/ Y):] iff
[x,y] in [:(X \/ Y),Z:] )
by Th87;
hence
(
[y,x] in [:Z,(X \/ Y):] iff
[y,x] in [:Z,X:] \/ [:Z,Y:] )
by A7, A9, XBOOLE_0:def 3;
verum
end;
A10:
for z being object st z in [:Z,(X \/ Y):] holds
ex x, y being object st z = [x,y]
by Lm19;
for z being object st z in [:Z,X:] \/ [:Z,Y:] holds
ex x, y being object st z = [x,y]
by A6;
hence
[:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:]
by A10, A8, Lm18; verum