let X be RealLinearSpace; :: thesis: for Y being Subspace of X
for v being Element of X
for v1 being Element of (RLSp2RVSp X) st v = v1 holds
v + Y = v1 + (RLSp2RVSp Y)
let Y be Subspace of X; :: thesis: for v being Element of X
for v1 being Element of (RLSp2RVSp X) st v = v1 holds
v + Y = v1 + (RLSp2RVSp Y)
let v be Element of X; :: thesis: for v1 being Element of (RLSp2RVSp X) st v = v1 holds
v + Y = v1 + (RLSp2RVSp Y)
let v1 be Element of (RLSp2RVSp X); :: thesis: ( v = v1 implies v + Y = v1 + (RLSp2RVSp Y) )
set V = RLSp2RVSp X;
set W = RLSp2RVSp Y;
assume A1: v = v1 ; :: thesis: v + Y = v1 + (RLSp2RVSp Y)
for x being object holds
( x in v + Y iff x in v1 + (RLSp2RVSp Y) )

proof

let x be object ; :: thesis: ( x in v + Y iff x in v1 + (RLSp2RVSp Y) )

hereby :: thesis: ( x in v1 + (RLSp2RVSp Y) implies x in v + Y )

assume x in v + Y ; :: thesis: x in v1 + (RLSp2RVSp Y)
then consider y being Point of X such that
A2: ( x = v + y & y in Y ) ;
reconsider y1 = y as Point of (RLSp2RVSp X) ;
A3: y1 in RLSp2RVSp Y by A2;
v + y = v1 + y1 by A1;
hence x in v1 + (RLSp2RVSp Y) by A2, A3; :: thesis: verum

end;

assume x in v1 + (RLSp2RVSp Y) ; :: thesis: x in v + Y
then consider y1 being Element of (RLSp2RVSp X) such that
A4: ( x = v1 + y1 & y1 in RLSp2RVSp Y ) ;
reconsider y = y1 as Point of X ;
A5: y in Y by A4;
v + y = v1 + y1 by A1;
hence x in v + Y by A4, A5; :: thesis: verum

end;

hence v + Y = v1 + (RLSp2RVSp Y) by TARSKI:2; :: thesis: verum