let n be Element of NAT ; :: thesis: for f being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n)
for X being convex Subset of (TOP-REAL n) holds f .: X is convex
let f be homogeneous additive Function of (TOP-REAL n),(TOP-REAL n); :: thesis: for X being convex Subset of (TOP-REAL n) holds f .: X is convex
let X be convex Subset of (TOP-REAL n); :: thesis: f .: X is convex
let p, q be Point of (TOP-REAL n); :: according to JORDAN1:def 1 :: thesis: ( not p in f .: X or not q in f .: X or LSeg p,q c= f .: X )
assume p in f .: X ; :: thesis: ( not q in f .: X or LSeg p,q c= f .: X )
then consider p0 being Point of (TOP-REAL n) such that
A1: p0 in X and
A2: p = f . p0 by FUNCT_2:116;
assume q in f .: X ; :: thesis: LSeg p,q c= f .: X
then consider q0 being Point of (TOP-REAL n) such that
A3: q0 in X and
A4: q = f . q0 by FUNCT_2:116;
A5: LSeg p,q = { (((1 - l) * p) + (l * q)) where l is Real : ( 0 <= l & l <= 1 ) } ;
A6: LSeg p0,q0 = { (((1 - l) * p0) + (l * q0)) where l is Real : ( 0 <= l & l <= 1 ) } ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg p,q or x in f .: X )
assume x in LSeg p,q ; :: thesis: x in f .: X
then consider l being Real such that
A7: x = ((1 - l) * p) + (l * q) and
A8: ( 0 <= l & l <= 1 ) by A5;
set a = ((1 - l) * p0) + (l * q0);
A9: ((1 - l) * p0) + (l * q0) in LSeg p0,q0 by A6, A8;
A10: LSeg p0,q0 c= X by A1, A3, JORDAN1:def 1;
f . (((1 - l) * p0) + (l * q0)) = (f . ((1 - l) * p0)) + (f . (l * q0)) by Def5
.= (f . ((1 - l) * p0)) + (l * (f . q0)) by Def4
.= x by A2, A4, A7, Def4 ;
hence x in f .: X by A9, A10, FUNCT_2:43; :: thesis: verum