let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let W1, W2 be Subspace of V; :: thesis: the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
thus the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1 :: according to XBOOLE_0:def 10 :: thesis: the carrier of W1 c= the carrier of (W1 /\ (W1 + W2))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 /\ (W1 + W2)) or x in the carrier of W1 )
assume A1: x in the carrier of (W1 /\ (W1 + W2)) ; :: thesis: x in the carrier of W1
the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 /\ the carrier of (W1 + W2) by Def2;
hence x in the carrier of W1 by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W1 or x in the carrier of (W1 /\ (W1 + W2)) )
assume A2: x in the carrier of W1 ; :: thesis: x in the carrier of (W1 /\ (W1 + W2))
the carrier of W1 c= the carrier of V by RLSUB_1:def 2;
then reconsider x1 = x as Element of V by A2;
A3: ( x1 + (0. V) = x1 & 0. V in W2 ) by RLSUB_1:17;
x in W1 by ;
then x in { (u + v) where v, u is VECTOR of V : ( u in W1 & v in W2 ) } by A3;
then x in the carrier of (W1 + W2) by Def1;
then x in the carrier of W1 /\ the carrier of (W1 + W2) by ;
hence x in the carrier of (W1 /\ (W1 + W2)) by Def2; :: thesis: verum