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))

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

thus
the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
by Lm8; :: thesis: verum
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 A1, A4, RLSUB_1:8;

x in the carrier of W2 by A2, XBOOLE_0:def 4;

then u1 + v1 in W2 by A3, STRUCT_0:def 5;

then (v1 + u1) - u1 in W2 by A6, RLSUB_1:23;

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 A5, Th3;

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;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 A1, A4, RLSUB_1:8;

x in the carrier of W2 by A2, XBOOLE_0:def 4;

then u1 + v1 in W2 by A3, STRUCT_0:def 5;

then (v1 + u1) - u1 in W2 by A6, RLSUB_1:23;

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 A5, Th3;

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