set i = id ([#] REAL );
thus REAL c= dom (id ([#] REAL )) by FUNCT_1:34; :: according to RFUNCT_3:def 13 :: thesis: for p being Real st 0 <= p & p <= 1 holds
for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
(id ([#] REAL )) . ((p * r) + ((1 - p) * s)) <= (p * ((id ([#] REAL )) . r)) + ((1 - p) * ((id ([#] REAL )) . s))
let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
(id ([#] REAL )) . ((p * r) + ((1 - p) * s)) <= (p * ((id ([#] REAL )) . r)) + ((1 - p) * ((id ([#] REAL )) . s)) )
assume ( 0 <= p & p <= 1 ) ; :: thesis: for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
(id ([#] REAL )) . ((p * r) + ((1 - p) * s)) <= (p * ((id ([#] REAL )) . r)) + ((1 - p) * ((id ([#] REAL )) . s))
let x, y be Real; :: thesis: ( x in REAL & y in REAL & (p * x) + ((1 - p) * y) in REAL implies (id ([#] REAL )) . ((p * x) + ((1 - p) * y)) <= (p * ((id ([#] REAL )) . x)) + ((1 - p) * ((id ([#] REAL )) . y)) )
assume ( x in REAL & y in REAL & (p * x) + ((1 - p) * y) in REAL ) ; :: thesis: (id ([#] REAL )) . ((p * x) + ((1 - p) * y)) <= (p * ((id ([#] REAL )) . x)) + ((1 - p) * ((id ([#] REAL )) . y))
( (id ([#] REAL )) . x = x & (id ([#] REAL )) . y = y & (id ([#] REAL )) . ((p * x) + ((1 - p) * y)) = (p * x) + ((1 - p) * y) ) by FUNCT_1:34;
hence (id ([#] REAL )) . ((p * x) + ((1 - p) * y)) <= (p * ((id ([#] REAL )) . x)) + ((1 - p) * ((id ([#] REAL )) . y)) ; :: thesis: verum