let X be RealNormSpace; :: thesis: for V being Subset of X
for a being Real
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
let V be Subset of X; :: thesis: for a being Real
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
let a be Real; :: thesis: for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
let V1 be Subset of (LinearTopSpaceNorm X); :: thesis: ( V = V1 implies a * V = a * V1 )
assume A1: V = V1 ; :: thesis: a * V = a * V1
thus a * V c= a * V1 :: according to XBOOLE_0:def 10 :: thesis: a * V1 c= a * V

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in a * V or z in a * V1 )
assume A3: z in a * V ; :: thesis: z in a * V1
consider v being Point of X such that
A4: ( z = a * v & v in V ) by A3;
reconsider v1 = v as Point of (LinearTopSpaceNorm X) by A1, A4;
a * v = a * v1 by NORMSP_2:def 4;
hence z in a * V1 by A1, A4; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in a * V1 or z in a * V )
assume B3: z in a * V1 ; :: thesis: z in a * V
consider v being Point of (LinearTopSpaceNorm X) such that
B4: ( z = a * v & v in V1 ) by B3;
reconsider v1 = v as Point of X by A1, B4;
a * v = a * v1 by NORMSP_2:def 4;
hence z in a * V by A1, B4; :: thesis: verum