let p be Real; :: thesis: ( 0<= p & p <= 1 implies for r, s being Real st r in X & s in X & (p * r)+((1 - p)* s)in X holds f .((p * r)+((1 - p)* s))<=(p *(f . r))+((1 - p)*(f . s)) ) assume A3:
( 0<= p & p <= 1 )
; :: thesis: for r, s being Real st r in X & s in X & (p * r)+((1 - p)* s)in X holds f .((p * r)+((1 - p)* s))<=(p *(f . r))+((1 - p)*(f . s))
for r, s being Real st r in X & s in X & (p * r)+((1 - p)* s)in X holds f .((p * r)+((1 - p)* s))<=(p *(f . r))+((1 - p)*(f . s))
hence
for r, s being Real st r in X & s in X & (p * r)+((1 - p)* s)in X holds f .((p * r)+((1 - p)* s))<=(p *(f . r))+((1 - p)*(f . s))
; :: thesis: verum