let X be RealLinearSpace; :: thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds
( f is convex iff for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

let f be Function of the carrier of X,ExtREAL; :: thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) )

assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis: ( f is convex iff for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

thus ( f is convex implies for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) :: thesis: ( ( for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) implies f is convex )
proof
assume A2: f is convex ; :: thesis: for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

let x1, x2 be VECTOR of X; :: thesis: for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

let p be Real; :: thesis: ( 0 <= p & p <= 1 implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )
assume that
A3: 0 <= p and
A4: p <= 1 ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
per cases ( p = 0 or p = 1 or ( p <> 0 & p <> 1 ) ) ;
suppose A5: p = 0 ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
then A6: (1 - p) * x2 = x2 by RLVECT_1:def 8;
p * x1 = 0. X by ;
then A7: (p * x1) + ((1 - p) * x2) = x2 by A6;
A8: (1 - p) * (f . x2) = f . x2 by ;
p * (f . x1) = 0. by A5;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by ; :: thesis: verum
end;
suppose A9: p = 1 ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
then A10: (1 - p) * x2 = 0. X by RLVECT_1:10;
p * x1 = x1 by ;
then A11: (p * x1) + ((1 - p) * x2) = x1 by A10;
A12: p * (f . x1) = f . x1 by ;
(1 - p) * (f . x2) = 0. by A9;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by ; :: thesis: verum
end;
suppose A13: ( p <> 0 & p <> 1 ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
then p < 1 by ;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A1, A2, A3, A13, Th4; :: thesis: verum
end;
end;
end;
assume for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ; :: thesis: f is convex
then for x1, x2 being VECTOR of X
for p being Real st 0 < p & p < 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ;
hence f is convex by ; :: thesis: verum