let K be Field; :: thesis: for V being VectSp of K
for W1, W2, W12 being Subspace of V
for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
let V be VectSp of K; :: thesis: for W1, W2, W12 being Subspace of V
for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
let W1, W2, W12 be Subspace of V; :: thesis: for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
let U1, U2 be Subspace of W12; :: thesis: ( U1 = W1 & U2 = W2 implies ( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 ) )
assume A1: ( U1 = W1 & U2 = W2 ) ; :: thesis: ( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
reconsider U12 = U1 /\ U2 as Subspace of V by VECTSP_4:34;
A2: the carrier of (W1 /\ W2) c= the carrier of U12

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 /\ W2) or x in the carrier of U12 )
assume A3: x in the carrier of (W1 /\ W2) ; :: thesis: x in the carrier of U12
x in W1 /\ W2 by A3, STRUCT_0:def 5;
then ( x in W1 & x in W2 ) by VECTSP_5:7;
then x in U12 by A1, VECTSP_5:7;
hence x in the carrier of U12 by STRUCT_0:def 5; :: thesis: verum

end;

the carrier of U12 c= the carrier of (W1 /\ W2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of U12 or x in the carrier of (W1 /\ W2) )
assume A4: x in the carrier of U12 ; :: thesis: x in the carrier of (W1 /\ W2)
x in U1 /\ U2 by A4, STRUCT_0:def 5;
then ( x in U1 & x in U2 ) by VECTSP_5:7;
then x in W1 /\ W2 by A1, VECTSP_5:7;
hence x in the carrier of (W1 /\ W2) by STRUCT_0:def 5; :: thesis: verum

end;

then the carrier of (W1 /\ W2) = the carrier of U12 by A2, XBOOLE_0:def 10;
hence W1 /\ W2 = U1 /\ U2 by VECTSP_4:37; :: thesis: W1 + W2 = U1 + U2
reconsider U12 = U1 + U2 as Subspace of V by VECTSP_4:34;
A5: the carrier of (W1 + W2) c= the carrier of U12

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of U12 )
assume A6: x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of U12
x in W1 + W2 by A6, STRUCT_0:def 5;
then consider v1, v2 being Vector of V such that
A7: ( v1 in W1 & v2 in W2 & v1 + v2 = x ) by VECTSP_5:5;
( U1 is Subspace of U12 & U2 is Subspace of U12 ) by VECTSP_5:11;
then ( v1 in U12 & v2 in U12 ) by A1, A7, VECTSP_4:16;
then reconsider w1 = v1, w2 = v2 as Vector of U12 by STRUCT_0:def 5;
v1 + v2 = w1 + w2 by VECTSP_4:21;
hence x in the carrier of U12 by A7; :: thesis: verum

end;

the carrier of U12 c= the carrier of (W1 + W2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of U12 or x in the carrier of (W1 + W2) )
assume A8: x in the carrier of U12 ; :: thesis: x in the carrier of (W1 + W2)
x in U1 + U2 by A8, STRUCT_0:def 5;
then consider v1, v2 being Vector of W12 such that
A9: ( v1 in U1 & v2 in U2 & v1 + v2 = x ) by VECTSP_5:5;
reconsider w1 = v1, w2 = v2 as Vector of V by VECTSP_4:18;
v1 + v2 = w1 + w2 by VECTSP_4:21;
then x in W1 + W2 by A1, A9, VECTSP_5:5;
hence x in the carrier of (W1 + W2) by STRUCT_0:def 5; :: thesis: verum

end;

then the carrier of (W1 + W2) = the carrier of U12 by A5, XBOOLE_0:def 10;
hence W1 + W2 = U1 + U2 by VECTSP_4:37; :: thesis: verum