let X, Y be RealNormSpace; :: thesis: for x being Point of X
for r being real number
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 number
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 number ; :: 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 )
assume A1: V = T .: (Ball x,r) ; :: thesis: V is convex
reconsider V1 = T .: (Ball x,r) as Subset of Y ;
K2: 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

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 A2: ( 0 < s & s < 1 & u in V1 & v in V1 ) ; :: thesis: (s * u) + ((1 - s) * v) in V1
consider z1 being set such that
A3: ( z1 in the carrier of X & z1 in Ball x,r & u = T . z1 ) by A2, FUNCT_2:115;
reconsider zz1 = z1 as Point of X by A3;
A6: s * u = T . (s * zz1) by A3, LOPBAN_1:def 6;
consider z2 being set such that
A7: ( z2 in the carrier of X & z2 in Ball x,r & v = T . z2 ) by A2, FUNCT_2:115;
reconsider zz2 = z2 as Point of X by A7;
A10: (1 - s) * v = T . ((1 - s) * zz2) by A7, LOPBAN_1:def 6;
reconsider za1 = zz1 as Point of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
reconsider za2 = zz2 as Point of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
reconsider Bxr = Ball x,r as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
Bxr is convex by Lm11;
then AM1: (s * za1) + ((1 - s) * za2) in Bxr by A2, A3, A7, CONVEX1:def 2;
AM2: s * za1 = s * zz1 by NORMSP_2:def 4;
AM3: (1 - s) * za2 = (1 - s) * zz2 by NORMSP_2:def 4;
AM4: (s * za1) + ((1 - s) * za2) = (s * zz1) + ((1 - s) * zz2) by AM2, AM3, NORMSP_2:def 4;
(s * u) + ((1 - s) * v) = T . ((s * zz1) + ((1 - s) * zz2)) by A6, A10, LOPBAN_1:def 5;
hence (s * u) + ((1 - s) * v) in V1 by AM1, AM4, FUNCT_2:43; :: thesis: verum

end;

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 )
assume ASV: ( 0 < s & s < 1 & u in V & v in V ) ; :: thesis: (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;
L2: s * u1 = s * u by NORMSP_2:def 4;
L3: (1 - s) * v1 = (1 - s) * v by NORMSP_2:def 4;
(s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by L2, L3, NORMSP_2:def 4;
hence (s * u) + ((1 - s) * v) in V by K2, A1, ASV; :: thesis: verum

end;

hence V is convex by CONVEX1:def 2; :: thesis: verum