let n be Nat; :: thesis: for f being additive homogeneous 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 additive homogeneous 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:65;
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:65;
A5: LSeg (p0,q0) c= X by A1, A3, JORDAN1:def 1;
let x be object ; :: 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
A6: x = ((1 - l) * p) + (l * q) and
A7: ( 0 <= l & l <= 1 ) ;
set a = ((1 - l) * p0) + (l * q0);
A8: ((1 - l) * p0) + (l * q0) in LSeg (p0,q0) by A7;
f . (((1 - l) * p0) + (l * q0)) = (f . ((1 - l) * p0)) + (f . (l * q0)) by VECTSP_1:def 20
.= (f . ((1 - l) * p0)) + (l * (f . q0)) by Def4
.= x by A2, A4, A6, Def4 ;
hence x in f .: X by A8, A5, FUNCT_2:35; :: thesis: verum