let V be RealNormSpace; :: thesis: for V1 being SubRealNormSpace of V
for S being Subset of V st S = the carrier of V1 holds
S is linearly-closed
let V1 be SubRealNormSpace of V; :: thesis: for S being Subset of V st S = the carrier of V1 holds
S is linearly-closed
let S be Subset of V; :: thesis: ( S = the carrier of V1 implies S is linearly-closed )
assume A1: S = the carrier of V1 ; :: thesis: S is linearly-closed
A2: for v, u being VECTOR of V st v in S & u in S holds
v + u in S

proof

let v, u be VECTOR of V; :: thesis: ( v in S & u in S implies v + u in S )
assume that
A3: v in S and
A4: u in S ; :: thesis: v + u in S
reconsider v1 = v, u1 = u as Point of V1 by A1, A3, A4;
v + u = v1 + u1 by SUBTH0;
hence v + u in S by A1; :: thesis: verum

end;

for r being Real
for v being VECTOR of V st v in S holds
r * v in S

proof

let r be Real; :: thesis: for v being VECTOR of V st v in S holds
r * v in S
let v be VECTOR of V; :: thesis: ( v in S implies r * v in S )
assume A5: v in S ; :: thesis: r * v in S
reconsider v1 = v as Point of V1 by A1, A5;
r * v = r * v1 by SUBTH0;
hence r * v in S by A1; :: thesis: verum

end;

hence S is linearly-closed by A2; :: thesis: verum