let X be RealLinearSpace; :: thesis: for Y1, Y2 being Subspace of X holds RLSp2RVSp (Y1 + Y2) = (RLSp2RVSp Y1) + (RLSp2RVSp Y2)
let Y1, Y2 be Subspace of X; :: thesis: RLSp2RVSp (Y1 + Y2) = (RLSp2RVSp Y1) + (RLSp2RVSp Y2)
set Y12 = Y1 + Y2;
A1: the carrier of (Y1 + Y2) = { (v + u) where u, v is VECTOR of X : ( v in Y1 & u in Y2 ) } by RLSUB_2:def 1;
A2: the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) = { (v + u) where u, v is Element of (RLSp2RVSp X) : ( v in RLSp2RVSp Y1 & u in RLSp2RVSp Y2 ) } by VECTSP_5:def 1;
A3: for x being object holds
( x in the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) iff x in the carrier of (RLSp2RVSp (Y1 + Y2)) )

proof

let x be object ; :: thesis: ( x in the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) iff x in the carrier of (RLSp2RVSp (Y1 + Y2)) )

hereby :: thesis: ( x in the carrier of (RLSp2RVSp (Y1 + Y2)) implies x in the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) )

assume x in the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) ; :: thesis: x in the carrier of (RLSp2RVSp (Y1 + Y2))
then consider u, v being Element of (RLSp2RVSp X) such that
A4: ( x = v + u & v in RLSp2RVSp Y1 & u in RLSp2RVSp Y2 ) by A2;
reconsider u1 = u, v1 = v as Element of X ;
A5: ( v1 in Y1 & u1 in Y2 ) by A4;
v + u = v1 + u1 ;
hence x in the carrier of (RLSp2RVSp (Y1 + Y2)) by A1, A4, A5; :: thesis: verum

end;

assume x in the carrier of (RLSp2RVSp (Y1 + Y2)) ; :: thesis: x in the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2))
then consider u, v being VECTOR of X such that
A6: ( x = v + u & v in Y1 & u in Y2 ) by A1;
reconsider v1 = v, u1 = u as Element of (RLSp2RVSp X) ;
A7: ( v in RLSp2RVSp Y1 & u in RLSp2RVSp Y2 ) by A6;
v + u = v1 + u1 ;
hence x in the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) by A2, A6, A7; :: thesis: verum

end;

A8: the addF of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) = the addF of (RLSp2RVSp X) || the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) by VECTSP_4:def 2
.= the addF of (RLSp2RVSp X) || the carrier of (RLSp2RVSp (Y1 + Y2)) by A3, TARSKI:2
.= the addF of (RLSp2RVSp (Y1 + Y2)) by VECTSP_4:def 2 ;
A9: 0. ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) = 0. (RLSp2RVSp X) by VECTSP_4:def 2
.= 0. (RLSp2RVSp (Y1 + Y2)) by VECTSP_4:def 2 ;
MultF_Real* (Y1 + Y2) = the Mult of X | [:REAL, the carrier of (Y1 + Y2):] by RLSUB_1:def 2
.= the lmult of (RLSp2RVSp X) | [: the carrier of F_Real, the carrier of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)):] by A3, TARSKI:2
.= the lmult of ((RLSp2RVSp Y1) + (RLSp2RVSp Y2)) by VECTSP_4:def 2 ;
hence RLSp2RVSp (Y1 + Y2) = (RLSp2RVSp Y1) + (RLSp2RVSp Y2) by A3, A8, A9, TARSKI:2; :: thesis: verum