let X be RealLinearSpace; :: thesis: for M, N being Subset of X
for r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N)
let M, N be Subset of X; :: thesis: for r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N)
let r be non zero Real; :: thesis: (r * M) /\ (r * N) = r * (M /\ N)
thus for x being object st x in (r * M) /\ (r * N) holds
x in r * (M /\ N) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: r * (M /\ N) c= (r * M) /\ (r * N)
proof
let x be object ; :: thesis: ( x in (r * M) /\ (r * N) implies x in r * (M /\ N) )
assume A1: x in (r * M) /\ (r * N) ; :: thesis: x in r * (M /\ N)
then x in r * M by XBOOLE_0:def 4;
then consider v1 being Point of X such that
A2: r * v1 = x and
A3: v1 in M ;
x in r * N by A1, XBOOLE_0:def 4;
then consider v2 being Point of X such that
A4: r * v2 = x and
A5: v2 in N ;
v1 = v2 by A2, A4, RLVECT_1:36;
then v1 in M /\ N by A3, A5, XBOOLE_0:def 4;
hence x in r * (M /\ N) by A2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (M /\ N) or x in (r * M) /\ (r * N) )
assume x in r * (M /\ N) ; :: thesis: x in (r * M) /\ (r * N)
then consider v being Point of X such that
A6: r * v = x and
A7: v in M /\ N ;
v in N by A7, XBOOLE_0:def 4;
then A8: x in r * N by A6;
v in M by A7, XBOOLE_0:def 4;
then x in r * M by A6;
hence x in (r * M) /\ (r * N) by A8, XBOOLE_0:def 4; :: thesis: verum