let V be RealUnitarySpace; :: thesis: for W being Subspace of V holds Up W is Subspace-like

let W be Subspace of V; :: thesis: Up W is Subspace-like

0. V in W by RUSUB_1:11;

hence 0. V in Up W ; :: according to RUSUB_4:def 7 :: thesis: for x, y being Element of V

for a being Real st x in Up W & y in Up W holds

( x + y in Up W & a * x in Up W )

thus for x, y being Element of V

for a being Real st x in Up W & y in Up W holds

( x + y in Up W & a * x in Up W ) :: thesis: verum

let W be Subspace of V; :: thesis: Up W is Subspace-like

0. V in W by RUSUB_1:11;

hence 0. V in Up W ; :: according to RUSUB_4:def 7 :: thesis: for x, y being Element of V

for a being Real st x in Up W & y in Up W holds

( x + y in Up W & a * x in Up W )

thus for x, y being Element of V

for a being Real st x in Up W & y in Up W holds

( x + y in Up W & a * x in Up W ) :: thesis: verum

proof

let x, y be Element of V; :: thesis: for a being Real st x in Up W & y in Up W holds

( x + y in Up W & a * x in Up W )

let a be Real; :: thesis: ( x in Up W & y in Up W implies ( x + y in Up W & a * x in Up W ) )

assume that

A1: x in Up W and

A2: y in Up W ; :: thesis: ( x + y in Up W & a * x in Up W )

reconsider x = x, y = y as Element of V ;

A3: x in W by A1;

then A4: a * x in W by RUSUB_1:15;

y in W by A2;

then x + y in W by A3, RUSUB_1:14;

hence ( x + y in Up W & a * x in Up W ) by A4; :: thesis: verum

end;( x + y in Up W & a * x in Up W )

let a be Real; :: thesis: ( x in Up W & y in Up W implies ( x + y in Up W & a * x in Up W ) )

assume that

A1: x in Up W and

A2: y in Up W ; :: thesis: ( x + y in Up W & a * x in Up W )

reconsider x = x, y = y as Element of V ;

A3: x in W by A1;

then A4: a * x in W by RUSUB_1:15;

y in W by A2;

then x + y in W by A3, RUSUB_1:14;

hence ( x + y in Up W & a * x in Up W ) by A4; :: thesis: verum