= 1/cp by A12,A11,XREAL_1:85; then A15: 1/(n+1) < p by A14,XXREAL_0:2; let m be Nat; assume n<=m; then A16: n+1 <= m+1 by XREAL_1:6; set m1 = m+1; 1/m1 <= 1/(n+1) by A16,XREAL_1:85; then A17: 1/m1 < p by A15,XXREAL_0:2; set oi = ].r3-1/m1,r3+1/m1.[; A18: r3 < r3+1/m1 by XREAL_1:29; then r3-1/m1 < r3 by XREAL_1:19; then r3 in oi by A18; then A19: X/\oi is non empty by A1,Th63; m in NAT by ORDINAL1:def 12; then ex m9 being Nat st m9 = m & seq.m = the Element of X/\].r3-1/(m9+ 1),r3+1/(m9+1).[ by A5; then seq.m in oi by A19,XBOOLE_0:def 4; then consider s such that A20: seq.m = s and A21: r3-1/m1 < s & s < r3+1/m1; -1/m1 < s-r3 & s-r3 < 1/m1 by A21,XREAL_1:19,20; then |.s-r3.| < 1/m1 by SEQ_2:1; hence |.seq.m-r3.|

f.y; take r; let s be ExtReal; assume s in f.:X; then ex x being object st x in X & x in X & s = f.x by FUNCT_2:64; hence thesis by A5,A6; end; given p being Real such that A7: p is UpperBound of f.:X; take p + 1; let y be object; assume y in dom f; then f.y in rng f by FUNCT_1:3; then f.y in f.:X by RELSET_1:22; then p >= f.y by A7,XXREAL_2:def 1; then A8: p+1 >= f.y+1 by XREAL_1:6; f.y < f.y + 1 by XREAL_1:29; hence thesis by A8,XXREAL_0:2; end; end; definition let X be set, f be Function of X, REAL; attr f is with_max means f.:X is with_max; attr f is with_min means f.:X is with_min; end; theorem Th65: for X, A being set, f being Function of X, REAL holds (-f).:A = --(f.:A) proof let X, A be set, f be Function of X, REAL; now let x be object; hereby assume x in (-f).:A; then consider x1 being object such that A1: x1 in X & x1 in A & x = (-f).x1 by FUNCT_2:64; x = -(f.x1) & f.x1 in f.:A by A1,FUNCT_2:35,VALUED_1:8; hence x in --(f.:A); end; assume x in --(f.:A); then consider r3 being Complex such that A2: x = -r3 and A3: r3 in f.:A; reconsider r3 as Real by A3; consider x1 being object such that A4: x1 in X & x1 in A and A5: r3 = f.x1 by A3,FUNCT_2:64; x = (-f).x1 by A2,A5,VALUED_1:8; hence x in (-f).:A by A4,FUNCT_2:35; end; hence thesis by TARSKI:2; end; Lm9: for X being non empty set, f being Function of X, REAL st f is with_max holds -f is with_min proof let X be non empty set, f be Function of X, REAL; assume that A1: f.:X is bounded_above and A2: upper_bound (f.:X) in f.:X; A3: --(f.:X) = (-f).:X by Th65; hence (-f).:X is bounded_below by A1,Lm2; then A4: lower_bound ((-f).:X) = - upper_bound -- --(f.:X) by A3,Th43 .= - upper_bound (f.:X); - upper_bound (f.:X) in --(f.:X) by A2; hence thesis by A4,Th65; end; Lm10: for X being non empty set, f being Function of X, REAL st f is with_min holds -f is with_max proof let X be non empty set, f be Function of X, REAL; assume that A1: f.:X is bounded_below and A2: lower_bound (f.:X) in f.:X; A3: --(f.:X) = (-f).:X by Th65; hence (-f).:X is bounded_above by A1,Lm3; then A4: upper_bound ((-f).:X) = - lower_bound -- --(f.:X) by A3,Th44 .= - lower_bound (f.:X); - lower_bound (f.:X) in --(f.:X) by A2; hence thesis by A4,Th65; end; theorem Th66: for X being non empty set, f being Function of X, REAL holds f is with_min iff -f is with_max proof let X be non empty set, f be Function of X, REAL; - -f = f; hence thesis by Lm9,Lm10; end; theorem for X being non empty set, f being Function of X, REAL holds f is with_max iff -f is with_min proof let X be non empty set, f be Function of X, REAL; - -f = f; hence thesis by Th66; end; theorem for X being set, A being Subset of REAL, f being Function of X, REAL holds (-f)"A = f"(--A) proof let X be set, A be Subset of REAL, f be Function of X, REAL; now let x be object; reconsider xx=x as set by TARSKI:1; hereby A1: (-f).x = -(f.xx) by VALUED_1:8; assume A2: x in (-f)"A; then (-f).x in A by FUNCT_2:38; then - -f.xx in --A by A1; hence x in f"(--A) by A2,FUNCT_2:38; end; A3: (-f).x = -(f.xx) by VALUED_1:8; assume A4: x in f"(--A); then f.x in --A by FUNCT_2:38; then (-f).x in -- --A by A3; hence x in (-f)"A by A4,FUNCT_2:38; end; hence thesis by TARSKI:2; end; theorem for X, A being set, f being Function of X, REAL, s being Real holds (s+f).:A = s++(f.:A) proof let X, A be set, f be Function of X, REAL, s be Real; now let x be object; hereby assume x in (s+f).:A; then consider x1 being object such that A1: x1 in X & x1 in A & x = (s+f).x1 by FUNCT_2:64; x = s+(f.x1) & f.x1 in f.:A by A1,FUNCT_2:35,VALUED_1:2; then x in { s + q3 : q3 in f.:A }; hence x in s++(f.:A) by Lm5; end; assume x in s++(f.:A); then x in { s + q3 : q3 in f.:A } by Lm5; then consider r3 such that A2: x = s+r3 and A3: r3 in f.:A; consider x1 being object such that A4: x1 in X and A5: x1 in A and A6: r3 = f.x1 by A3,FUNCT_2:64; x = (s+f).x1 by A2,A4,A6,VALUED_1:2; hence x in (s+f).:A by A4,A5,FUNCT_2:35; end; hence thesis by TARSKI:2; end; theorem for X being set, A being Subset of REAL, f being Function of X,REAL, q3 holds (q3+f)"A = f"(-q3++A) proof let X be set, A be Subset of REAL, f be Function of X, REAL, q3 be Real; now let x be object; reconsider xx=x as set by TARSKI:1; hereby assume A1: x in (q3+f)"A; then (q3+f).x in A & (q3+f).x = q3+(f.xx) by FUNCT_2:38,VALUED_1:2; then -q3+(q3+(f.xx)) in { -q3 + p3 : p3 in A }; then -q3+(q3+(f.xx)) in -q3++A by Lm5; hence x in f"(-q3++A) by A1,FUNCT_2:38; end; assume A2: x in f"(-q3++A); then f.x in -q3++A & (q3+f).x = q3+(f.xx) by FUNCT_2:38,VALUED_1:2; then (q3+f).x in { q3+p3 : p3 in -q3 ++ A }; then (q3+f).x in q3++(-q3++A) by Lm5; then (q3+f).x in (q3+-q3)++A by MEMBER_1:147; then (q3+f).x in A by MEMBER_1:146; hence x in (q3+f)"A by A2,FUNCT_2:38; end; hence thesis by TARSKI:2; end; notation let f be real-valued Function; synonym Inv f for f"; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; redefine func Inv f -> PartFunc of C,REAL; coherence proof f" is PartFunc of C,REAL; hence thesis; end; end; theorem for X being set, A being without_zero Subset of REAL, f being Function of X, REAL holds (Inv f)"A = f"(Inv A) proof let X be set, A be without_zero Subset of REAL, f be Function of X, REAL; now let x be object; reconsider xx=x as set by TARSKI:1; hereby A1: (Inv f).x = (f.xx)" by VALUED_1:10; assume A2: x in (Inv f)"A; then (Inv f).x in A by FUNCT_2:38; then 1/((f.xx)") in Inv A by A1; hence x in f"(Inv A) by A2,FUNCT_2:38; end; A3: (f.xx)" = 1/(f.xx) & (Inv f).x = (f.xx)" by VALUED_1:10; assume A4: x in f"(Inv A); then f.x in Inv A by FUNCT_2:38; then (Inv f).x in Inv Inv A by A3; hence x in (Inv f)"A by A4,FUNCT_2:38; end; hence thesis by TARSKI:2; end; theorem for A being Subset of REAL, x being Real st x in --A holds ex a being Real st a in A & x = -a proof let A be Subset of REAL, x be Real; assume x in --A; then x in {-a where a is Complex: a in A}; then consider a being Complex such that A1: x = -a & a in A; reconsider a as Real by A1; take a; thus thesis by A1; end;