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

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

hence
v + Y = v1 + (RLSp2RVSp Y)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in v + Y iff x in v1 + (RLSp2RVSp 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;hereby :: thesis: ( x in v1 + (RLSp2RVSp Y) implies x in v + Y )

assume
x in v1 + (RLSp2RVSp Y)
; :: thesis: x in v + Yassume
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;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

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