let X, Y be RealNormSpace; :: thesis: for x being Point of X
for r being Real
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let x be Point of X; :: thesis: for r being Real
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let r be Real; :: thesis: for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let T be LinearOperator of X,Y; :: thesis: for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let V be Subset of (LinearTopSpaceNorm Y); :: thesis: ( V = T .: (Ball (x,r)) implies V is convex )
reconsider V1 = T .: (Ball (x,r)) as Subset of Y ;
A1: for u, v being Point of Y
for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1

proof

reconsider Bxr = Ball (x,r) as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
let u, v be Point of Y; :: thesis: for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1
let s be Real; :: thesis: ( 0 < s & s < 1 & u in V1 & v in V1 implies (s * u) + ((1 - s) * v) in V1 )
assume that
A2: ( 0 < s & s < 1 ) and
A3: u in V1 and
A4: v in V1 ; :: thesis: (s * u) + ((1 - s) * v) in V1
consider z1 being object such that
A5: z1 in the carrier of X and
A6: z1 in Ball (x,r) and
A7: u = T . z1 by A3, FUNCT_2:64;
reconsider zz1 = z1 as Point of X by A5;
reconsider za1 = zz1 as Point of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
consider z2 being object such that
A8: z2 in the carrier of X and
A9: z2 in Ball (x,r) and
A10: v = T . z2 by A4, FUNCT_2:64;
reconsider zz2 = z2 as Point of X by A8;
A11: (1 - s) * v = T . ((1 - s) * zz2) by A10, LOPBAN_1:def 5;
reconsider za2 = zz2 as Point of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
( s * za1 = s * zz1 & (1 - s) * za2 = (1 - s) * zz2 ) by NORMSP_2:def 4;
then A12: (s * za1) + ((1 - s) * za2) = (s * zz1) + ((1 - s) * zz2) by NORMSP_2:def 4;
s * u = T . (s * zz1) by A7, LOPBAN_1:def 5;
then A13: (s * u) + ((1 - s) * v) = T . ((s * zz1) + ((1 - s) * zz2)) by A11, VECTSP_1:def 20;
Bxr is convex by Th12;
then (s * za1) + ((1 - s) * za2) in Bxr by A2, A6, A9;
hence (s * u) + ((1 - s) * v) in V1 by A12, A13, FUNCT_2:35; :: thesis: verum

end;

assume A14: V = T .: (Ball (x,r)) ; :: thesis: V is convex
for u, v being Point of (LinearTopSpaceNorm Y)
for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V

proof

let u, v be Point of (LinearTopSpaceNorm Y); :: thesis: for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V
let s be Real; :: thesis: ( 0 < s & s < 1 & u in V & v in V implies (s * u) + ((1 - s) * v) in V )
reconsider u1 = u as Point of Y by NORMSP_2:def 4;
reconsider v1 = v as Point of Y by NORMSP_2:def 4;
( s * u1 = s * u & (1 - s) * v1 = (1 - s) * v ) by NORMSP_2:def 4;
then A15: (s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by NORMSP_2:def 4;
assume ( 0 < s & s < 1 & u in V & v in V ) ; :: thesis: (s * u) + ((1 - s) * v) in V
hence (s * u) + ((1 - s) * v) in V by A14, A1, A15; :: thesis: verum

end;

hence V is convex ; :: thesis: verum