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

for v being VECTOR of V st v in S holds

r * v in S

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

for r being Real
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;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

for v being VECTOR of V st v in S holds

r * v in S

proof

hence
S is linearly-closed
by A2; :: thesis: verum
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;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