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 object ; :: according to TARSKI:def 3 :: thesis: ( not z in a * V or z in a * V1 )
assume z in a * V ; :: thesis: z in a * V1
then consider v being Point of X such that
A2: z = a * v and
A3: v in V ;
reconsider v1 = v as Point of (LinearTopSpaceNorm X) by A1, A3;
a * v = a * v1 by NORMSP_2:def 4;
hence z in a * V1 by A1, A2, A3; :: thesis: verum

end;

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