let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st f is_strictly_quasiconvex_on X & f is one-to-one holds
f is_strongly_quasiconvex_on X
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_strictly_quasiconvex_on X & f is one-to-one implies f is_strongly_quasiconvex_on X )
assume that
A1: f is_strictly_quasiconvex_on X and
A2: f is one-to-one ; :: thesis: f is_strongly_quasiconvex_on X
A3: X c= dom f by A1, Def3;
for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s)

proof

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 & r <> s holds
f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s) )
assume A4: ( 0 < p & p < 1 ) ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s)
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s)

proof

let r, s be Real; :: thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s) )
assume that
A5: ( r in X & s in X ) and
A6: (p * r) + ((1 - p) * s) in X and
A7: r <> s ; :: thesis: f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s)
f . r <> f . s by A2, A3, A5, A7, FUNCT_1:def 8;
hence f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s) by A1, A4, A5, A6, Def3; :: thesis: verum

end;

hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s) ; :: thesis: verum

end;

hence f is_strongly_quasiconvex_on X by A3, Def4; :: thesis: verum