let X, Y, Z be set ; :: thesis: ( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )
thus A1: [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] :: thesis: [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:]

proof

A2: ( [:(X /\ Y),Z:] c= [:(X /\ Y),Z:] & [:X,Z:] /\ [:Y,Z:] c= [:X,Z:] ) by XBOOLE_1:17;
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 & x in Y & y in Z ) by XBOOLE_0:def 4;
then ( [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] ) by Lm17;
hence [x,y] in [:X,Z:] /\ [:Y,Z:] by XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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

end;

A3: ( [:Z,(X /\ Y):] c= [:Z,(X /\ Y):] & [:Z,X:] /\ [:Z,Y:] c= [:Z,X:] ) by XBOOLE_1:17;
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):] ) & ( [x,y] in [:X,Z:] /\ [:Y,Z:] implies ( [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] ) ) & ( [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] implies [x,y] in [:X,Z:] /\ [:Y,Z:] ) & ( [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] implies ( [y,x] in [:Z,X:] & [y,x] in [:Z,Y:] ) ) & ( [y,x] in [:Z,X:] & [y,x] in [:Z,Y:] implies ( [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] ) ) ) by Th107, XBOOLE_0:def 4;
hence ( [y,x] in [:Z,(X /\ Y):] iff [y,x] in [:Z,X:] /\ [:Z,Y:] ) by A1, XBOOLE_0:def 4; :: thesis: verum

end;

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