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