set i = id ([#] REAL);
thus REAL c= dom (id ([#] REAL)) by FUNCT_1:17; :: according to RFUNCT_3:def 12 :: 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 that
0 <= p and
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 that
A1: x in REAL and
A2: y in REAL and
A3: (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 ) by A1, A2, FUNCT_1:17;
hence (id ([#] REAL)) . ((p * x) + ((1 - p) * y)) <= (p * ((id ([#] REAL)) . x)) + ((1 - p) * ((id ([#] REAL)) . y)) by A3, FUNCT_1:17; :: thesis: verum