let V be RealLinearSpace; :: thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))

let W1, W2, W3 be Subspace of V; :: thesis: ( W1 is Subspace of W2 implies the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume A1: W1 is Subspace of W2 ; :: thesis: the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
thus the carrier of (W2 /\ (W1 + W3)) c= the carrier of ((W1 /\ W2) + (W2 /\ W3)) :: according to XBOOLE_0:def 10 :: thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W2 /\ (W1 + W3)) or x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume x in the carrier of (W2 /\ (W1 + W3)) ; :: thesis: x in the carrier of ((W1 /\ W2) + (W2 /\ W3))
then A2: x in the carrier of W2 /\ the carrier of (W1 + W3) by Def2;
then x in the carrier of (W1 + W3) by XBOOLE_0:def 4;
then x in { (u + v) where v, u is VECTOR of V : ( u in W1 & v in W3 ) } by Def1;
then consider v1, u1 being VECTOR of V such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3 ;
A6: u1 in W2 by ;
x in the carrier of W2 by ;
then u1 + v1 in W2 by ;
then (v1 + u1) - u1 in W2 by ;
then v1 + (u1 - u1) in W2 by RLVECT_1:def 3;
then v1 + (0. V) in W2 by RLVECT_1:15;
then v1 in W2 ;
then A7: v1 in W2 /\ W3 by ;
u1 in W1 /\ W2 by A4, A6, Th3;
then x in (W1 /\ W2) + (W2 /\ W3) by A3, A7, Th1;
hence x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) by STRUCT_0:def 5; :: thesis: verum
end;
thus the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) by Lm8; :: thesis: verum