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

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

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 * V1 or z in a * V )
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;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

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