let X, Y, Z be set ; ( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )
A1:
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 A2:
[x,y] in [:(X /\ Y),Z:]
;
[x,y] in [:X,Z:] /\ [:Y,Z:]
then A3:
x in X /\ Y
by Lm16;
A4:
y in Z
by A2, Lm16;
x in Y
by A3, XBOOLE_0:def 4;
then A5:
[x,y] in [:Y,Z:]
by A4, Lm16;
x in X
by A3, XBOOLE_0:def 4;
then
[x,y] in [:X,Z:]
by A4, Lm16;
hence
[x,y] in [:X,Z:] /\ [:Y,Z:]
by A5, XBOOLE_0:def 4;
verum
end;
assume A6:
[x,y] in [:X,Z:] /\ [:Y,Z:]
;
[x,y] in [:(X /\ Y),Z:]
then
[x,y] in [:Y,Z:]
by XBOOLE_0:def 4;
then A7:
x in Y
by Lm16;
A8:
[x,y] in [:X,Z:]
by A6, XBOOLE_0:def 4;
then
x in X
by Lm16;
then A9:
x in X /\ Y
by A7, XBOOLE_0:def 4;
y in Z
by A8, Lm16;
hence
[x,y] in [:(X /\ Y),Z:]
by A9, Lm16;
verum
end;
[:X,Z:] /\ [:Y,Z:] c= [:X,Z:]
by XBOOLE_1:17;
hence A10:
[:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:]
by A1, Lm17; [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:]
A11:
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:] )
A12:
(
[x,y] in [:X,Z:] &
[x,y] in [:Y,Z:] iff (
[y,x] in [:Z,X:] &
[y,x] in [:Z,Y:] ) )
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 A10, A12, XBOOLE_0:def 4;
verum
end;
[:Z,X:] /\ [:Z,Y:] c= [:Z,X:]
by XBOOLE_1:17;
hence
[:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:]
by A11, Lm17; verum