let X be RealLinearSpace; :: thesis: for Y being Subspace of X
for v being Element of X
for v1 being Element of () st v = v1 holds
v + Y = v1 + ()

let Y be Subspace of X; :: thesis: for v being Element of X
for v1 being Element of () st v = v1 holds
v + Y = v1 + ()

let v be Element of X; :: thesis: for v1 being Element of () st v = v1 holds
v + Y = v1 + ()

let v1 be Element of (); :: thesis: ( v = v1 implies v + Y = v1 + () )
set V = RLSp2RVSp X;
set W = RLSp2RVSp Y;
assume A1: v = v1 ; :: thesis: v + Y = v1 + ()
for x being object holds
( x in v + Y iff x in v1 + () )
proof
let x be object ; :: thesis: ( x in v + Y iff x in v1 + () )
hereby :: thesis: ( x in v1 + () implies x in v + Y )
assume x in v + Y ; :: thesis: x in v1 + ()
then consider y being Point of X such that
A2: ( x = v + y & y in Y ) ;
reconsider y1 = y as Point of () ;
A3: y1 in RLSp2RVSp Y by A2;
v + y = v1 + y1 by A1;
hence x in v1 + () by A2, A3; :: thesis: verum
end;
assume x in v1 + () ; :: thesis: x in v + Y
then consider y1 being Element of () 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 + () by TARSKI:2; :: thesis: verum