:: The Limit of a Composition of Real Functions :: by Jaros{\l}aw Kotowicz :: :: Received September 5, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies REAL_1, PARTFUN1, NUMBERS, CARD_1, ARYTM_3, ARYTM_1, SEQ_1, RELAT_1, TARSKI, FUNCT_2, SUBSET_1, FUNCT_1, XBOOLE_0, LIMFUNC1, LIMFUNC2, SEQ_2, ORDINAL2, XXREAL_1, XXREAL_0, NAT_1, LIMFUNC3; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, SEQ_1, SEQ_2, VALUED_0, RCOMP_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, LIMFUNC1, LIMFUNC2, LIMFUNC3; constructors PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_2, LIMFUNC1, LIMFUNC2, LIMFUNC3, MEMBERED, RELSET_1, COMSEQ_2; registrations RELSET_1, VALUED_0, ORDINAL1, NUMBERS, XBOOLE_0, SEQ_4, FUNCT_2, XREAL_0, NAT_1; requirements SUBSET, ARITHM, BOOLE, NUMERALS; definitions TARSKI; equalities PROB_1, LIMFUNC1; expansions TARSKI, LIMFUNC1; theorems TARSKI, NAT_1, FUNCT_1, SEQ_4, RCOMP_1, LIMFUNC1, LIMFUNC2, LIMFUNC3, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_1, FUNCT_2, VALUED_0, ORDINAL1; begin reserve r,r1,r2,g,g1,g2,x0 for Real; reserve f1,f2 for PartFunc of REAL,REAL; Lm1: 0 < g implies r-glim(f1,x0)) implies f2*f1 is_divergent_to+infty_in x0 proof assume that A1: f1 is_convergent_in x0 and A2: f2 is_divergent_to+infty_in lim(f1,x0) and A3: for r1,r2 st r1lim(f1, x0); now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)\{x0}; consider k be Element of NAT such that A8: for n being Element of NAT st k<=n holds x0-glim(f1,x0) by A5; then A18: not f1.(s.(n+k)) in {lim(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11; hence x in dom f2\{lim(f1,x0)} by A18,A15,XBOOLE_0:def 5; end; then A19: rng q c=dom f2\{lim(f1,x0)}; lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4; then lim q=lim(f1,x0) by A12,SEQ_4:20; then f2/*q is divergent_to+infty by A2,A12,A19,LIMFUNC3:def 2; hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7; end; hence thesis by A3,LIMFUNC3:def 2; end; theorem f1 is_convergent_in x0 & f2 is_divergent_to-infty_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0)) implies f2*f1 is_divergent_to-infty_in x0 proof assume that A1: f1 is_convergent_in x0 and A2: f2 is_divergent_to-infty_in lim(f1,x0) and A3: for r1,r2 st r1lim(f1, x0); now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)\{x0}; consider k be Element of NAT such that A8: for n being Element of NAT st k<=n holds x0-glim(f1,x0) by A5; then A18: not f1.(s.(n+k)) in {lim(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11; hence x in dom f2\{lim(f1,x0)} by A18,A15,XBOOLE_0:def 5; end; then A19: rng q c=dom f2\{lim(f1,x0)}; lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4; then lim q=lim(f1,x0) by A12,SEQ_4:20; then f2/*q is divergent_to-infty by A2,A12,A19,LIMFUNC3:def 3; hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7; end; hence thesis by A3,LIMFUNC3:def 3; end; theorem f1 is_convergent_in x0 & f2 is_right_divergent_to+infty_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0)) implies f2*f1 is_divergent_to+infty_in x0 proof assume that A1: f1 is_convergent_in x0 and A2: f2 is_right_divergent_to+infty_in lim(f1,x0) and A3: for r1,r2 st r1lim(f1,x0) by A5; then f1.(s.(n+k)) in {g2: lim(f1,x0)lim(f1,x0)) implies f2*f1 is_divergent_to-infty_in x0 proof assume that A1: f1 is_convergent_in x0 and A2: f2 is_right_divergent_to-infty_in lim(f1,x0) and A3: for r1,r2 st r1lim(f1,x0) by A5; then f1.(s.(n+k)) in {g2: lim(f1,x0)lim_right(f1,x0)) implies f2*f1 is_right_divergent_to+infty_in x0 proof assume that A1: f1 is_right_convergent_in x0 and A2: f2 is_divergent_to+infty_in lim_right(f1,x0) and A3: for r st x0lim_right(f1,x0); now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)/\right_open_halfline(x0); consider k be Nat such that A8: for n be Nat st k<=n holds s.nlim_right(f1,x0) by A5; then A20: not f1.(s.(n+k)) in {lim_right(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11; hence x in dom f2\{lim_right(f1,x0)} by A20,A17,XBOOLE_0:def 5; end; then A21: rng q c=dom f2\{lim_right(f1,x0)}; lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8; then lim q=lim_right(f1,x0) by A12,SEQ_4:20; then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC3:def 2; hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7; end; hence thesis by A3,LIMFUNC2:def 5; end; theorem f1 is_right_convergent_in x0 & f2 is_divergent_to-infty_in lim_right( f1,x0 ) & (for r st x0lim_right(f1,x0)) implies f2*f1 is_right_divergent_to-infty_in x0 proof assume that A1: f1 is_right_convergent_in x0 and A2: f2 is_divergent_to-infty_in lim_right(f1,x0) and A3: for r st x0lim_right(f1,x0); now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)/\right_open_halfline(x0); consider k be Nat such that A8: for n be Nat st k<=n holds s.nlim_right(f1,x0) by A5; then A20: not f1.(s.(n+k)) in {lim_right(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11; hence x in dom f2\{lim_right(f1,x0)} by A20,A17,XBOOLE_0:def 5; end; then A21: rng q c=dom f2\{lim_right(f1,x0)}; lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8; then lim q=lim_right(f1,x0) by A12,SEQ_4:20; then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC3:def 3; hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7; end; hence thesis by A3,LIMFUNC2:def 6; end; theorem f1 is convergent_in+infty & f2 is_divergent_to+infty_in lim_in+infty f1 & (for r ex g st rlim_in+infty f1) implies f2*f1 is divergent_in+infty_to+infty proof assume that A1: f1 is convergent_in+infty and A2: f2 is_divergent_to+infty_in lim_in+infty f1 and A3: for r ex g st r lim_in+infty f1; now let s be Real_Sequence; assume that A5: s is divergent_to+infty and A6: rng s c=dom(f2*f1); consider k be Nat such that A7: for n be Nat st k<=n holds rlim_in+infty f1 by A4; then A16: not f1.(s.(n+k)) in {lim_in+infty f1} by TARSKI:def 1; A17: n+k in NAT by ORDINAL1:def 12; (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28; then (f1/*s).(n+k) in dom f2 by A8; then x in dom f2 by A10,A14,FUNCT_2:108,A17; hence thesis by A14,A16,XBOOLE_0:def 5; end; rng q c=dom f1 by A10,A11; then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9, LIMFUNC1:def 12; then A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC3:def 2; f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27 .=(f2/*(f1/*s))^\k by A8,VALUED_0:27 .=((f2*f1)/*s)^\k by A6,VALUED_0:31; hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7; end; hence thesis by A3; end; theorem f1 is convergent_in+infty & f2 is_divergent_to-infty_in lim_in+infty f1 & (for r ex g st rlim_in+infty f1) implies f2*f1 is divergent_in+infty_to-infty proof assume that A1: f1 is convergent_in+infty and A2: f2 is_divergent_to-infty_in lim_in+infty f1 and A3: for r ex g st r lim_in+infty f1; now let s be Real_Sequence; assume that A5: s is divergent_to+infty and A6: rng s c=dom(f2*f1); consider k being Nat such that A7: for n being Nat st k<=n holds rlim_in+infty f1 by A4; then A16: not f1.(s.(n+k)) in {lim_in+infty f1} by TARSKI:def 1; A17: n+k in NAT by ORDINAL1:def 12; (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28; then (f1/*s).(n+k) in dom f2 by A8; then x in dom f2 by A10,A14,FUNCT_2:108,A17; hence thesis by A14,A16,XBOOLE_0:def 5; end; rng q c=dom f1 by A10,A11; then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9, LIMFUNC1:def 12; then A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC3:def 3; f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27 .=(f2/*(f1/*s))^\k by A8,VALUED_0:27 .=((f2*f1)/*s)^\k by A6,VALUED_0:31; hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7; end; hence thesis by A3; end; theorem f1 is convergent_in-infty & f2 is_divergent_to+infty_in lim_in-infty f1 & (for r ex g st glim_in-infty f1) implies f2*f1 is divergent_in-infty_to+infty proof assume that A1: f1 is convergent_in-infty and A2: f2 is_divergent_to+infty_in lim_in-infty f1 and A3: for r ex g st glim_in-infty f1; now let s be Real_Sequence; assume that A5: s is divergent_to-infty and A6: rng s c=dom(f2*f1); consider k being Nat such that A7: for n being Nat st k<=n holds s.nlim_in-infty f1 by A4; then A16: not f1.(s.(n+k)) in {lim_in-infty f1} by TARSKI:def 1; A17: n+k in NAT by ORDINAL1:def 12; (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28; then (f1/*s).(n+k) in dom f2 by A8; then x in dom f2 by A10,A14,FUNCT_2:108,A17; hence thesis by A14,A16,XBOOLE_0:def 5; end; rng q c=dom f1 by A10,A11; then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9, LIMFUNC1:def 13; then A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC3:def 2; f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27 .=(f2/*(f1/*s))^\k by A8,VALUED_0:27 .=((f2*f1)/*s)^\k by A6,VALUED_0:31; hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7; end; hence thesis by A3; end; theorem f1 is convergent_in-infty & f2 is_divergent_to-infty_in lim_in-infty f1 & (for r ex g st glim_in-infty f1) implies f2*f1 is divergent_in-infty_to-infty proof assume that A1: f1 is convergent_in-infty and A2: f2 is_divergent_to-infty_in lim_in-infty f1 and A3: for r ex g st glim_in-infty f1; now let s be Real_Sequence; assume that A5: s is divergent_to-infty and A6: rng s c=dom(f2*f1); consider k being Nat such that A7: for n being Nat st k<=n holds s.nlim_in-infty f1 by A4; then A16: not f1.(s.(n+k)) in {lim_in-infty f1} by TARSKI:def 1; A17: n+k in NAT by ORDINAL1:def 12; (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28; then (f1/*s).(n+k) in dom f2 by A8; then x in dom f2 by A10,A14,FUNCT_2:108,A17; hence thesis by A14,A16,XBOOLE_0:def 5; end; rng q c=dom f1 by A10,A11; then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9, LIMFUNC1:def 13; then A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC3:def 3; f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27 .=(f2/*(f1/*s))^\k by A8,VALUED_0:27 .=((f2*f1)/*s)^\k by A6,VALUED_0:31; hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7; end; hence thesis by A3; end; theorem f1 is_convergent_in x0 & f2 is_left_divergent_to+infty_in lim(f1,x0) & (for r1,r2 st r1f1 .r; now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)\{x0}; consider k being Element of NAT such that A8: for n being Element of NAT st k<=n holds x0-gf1 .r; now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)\{x0}; consider k being Element of NAT such that A8: for n being Element of NAT st k<=n holds x0-glim_left(f1,x0)) implies f2*f1 is_left_divergent_to+infty_in x0 proof assume that A1: f1 is_left_convergent_in x0 and A2: f2 is_divergent_to+infty_in lim_left(f1,x0) and A3: for r st rlim_left(f1,x0); now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)/\left_open_halfline(x0); consider k being Nat such that A8: for n being Nat st k<=n holds x0-glim_left(f1,x0) by A5; then A20: not f1.(s.(n+k)) in {lim_left(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11; hence x in dom f2\{lim_left(f1,x0)} by A20,A17,XBOOLE_0:def 5; end; then A21: rng q c=dom f2\{lim_left(f1,x0)}; lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7; then lim q=lim_left(f1,x0) by A12,SEQ_4:20; then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC3:def 2; hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7; end; hence thesis by A3,LIMFUNC2:def 2; end; theorem f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in lim_left(f1, x0) & (for r st rlim_left(f1,x0)) implies f2*f1 is_left_divergent_to-infty_in x0 proof assume that A1: f1 is_left_convergent_in x0 and A2: f2 is_divergent_to-infty_in lim_left(f1,x0) and A3: for r st rlim_left(f1,x0); now let s be Real_Sequence; assume that A6: s is convergent & lim s=x0 and A7: rng s c=dom(f2*f1)/\left_open_halfline(x0); consider k being Nat such that A8: for n being Nat st k<=n holds x0-glim_left(f1,x0) by A5; then A20: not f1.(s.(n+k)) in {lim_left(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11; hence x in dom f2\{lim_left(f1,x0)} by A20,A17,XBOOLE_0:def 5; end; then A21: rng q c=dom f2\{lim_left(f1,x0)}; lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7; then lim q=lim_left(f1,x0) by A12,SEQ_4:20; then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC3:def 3; hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7; end; hence thesis by A3,LIMFUNC2:def 3; end; theorem f1 is divergent_in+infty_to+infty & f2 is convergent_in+infty & (for r ex g st rlim_in+infty f1) implies f2*f1 is convergent_in+infty & lim_in+infty(f2*f1)=lim(f2,lim_in+infty f1) proof assume that A1: f1 is convergent_in+infty and A2: f2 is_convergent_in lim_in+infty f1 and A3: for r ex g st r lim_in+infty f1; A5: now set L=lim(f2,lim_in+infty f1); let s be Real_Sequence; assume that A6: s is divergent_to+infty and A7: rng s c=dom(f2*f1); consider k being Nat such that A8: for n being Nat st k<=n holds rlim_in+infty f1 by A4; then A18: not f1.(s.(n+k)) in {lim_in+infty f1} by TARSKI:def 1; A19: n+k in NAT by ORDINAL1:def 12; (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28; then (f1/*s).(n+k) in dom f2 by A13; then x in dom f2 by A10,A16,FUNCT_2:108,A19; hence thesis by A16,A18,XBOOLE_0:def 5; end; A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27 .=(f2/*(f1/*s))^\k by A13,VALUED_0:27 .=((f2*f1)/*s)^\k by A7,VALUED_0:31; L=L; then A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC3:def 4; hence (f2*f1)/*s is convergent by A20,SEQ_4:21; lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC3:def 4; hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22; end; hence f2*f1 is convergent_in+infty by A3; hence thesis by A5,LIMFUNC1:def 12; end; theorem f1 is convergent_in-infty & f2 is_convergent_in lim_in-infty f1 & (for r ex g st glim_in-infty f1) implies f2*f1 is convergent_in-infty & lim_in-infty(f2*f1)=lim(f2,lim_in-infty f1) proof assume that A1: f1 is convergent_in-infty and A2: f2 is_convergent_in lim_in-infty f1 and A3: for r ex g st glim_in-infty f1; A5: now set L=lim(f2,lim_in-infty f1); let s be Real_Sequence; assume that A6: s is divergent_to-infty and A7: rng s c=dom(f2*f1); consider k being Nat such that A8: for n being Nat st k<=n holds s.nlim_in-infty f1 by A4; then A18: not f1.(s.(n+k)) in {lim_in-infty f1} by TARSKI:def 1; A19: n+k in NAT by ORDINAL1:def 12; (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28; then (f1/*s).(n+k) in dom f2 by A13; then x in dom f2 by A10,A16,FUNCT_2:108,A19; hence thesis by A16,A18,XBOOLE_0:def 5; end; A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27 .=(f2/*(f1/*s))^\k by A13,VALUED_0:27 .=((f2*f1)/*s)^\k by A7,VALUED_0:31; L=L; then A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC3:def 4; hence (f2*f1)/*s is convergent by A20,SEQ_4:21; lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC3:def 4; hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22; end; hence f2*f1 is convergent_in-infty by A3; hence thesis by A5,LIMFUNC1:def 13; end; theorem f1 is_convergent_in x0 & f2 is_left_convergent_in lim(f1,x0) & (for r1 ,r2 st r1lim_left(f1,x0)) implies f2*f1 is_left_convergent_in x0 & lim_left(f2*f1,x0)=lim(f2,lim_left(f1,x0)) proof assume that A1: f1 is_left_convergent_in x0 and A2: f2 is_convergent_in lim_left(f1,x0) and A3: for r st rlim_left(f1,x0); A6: now let s be Real_Sequence; assume that A7: s is convergent & lim s=x0 and A8: rng s c=dom(f2*f1)/\left_open_halfline(x0); consider k being Nat such that A9: for n being Nat st k<=n holds x0-glim_left(f1,x0) by A5; then A18: not f1.(s.(n+k)) in {lim_left(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11; hence x in dom f2\{lim_left(f1,x0)} by A18,A15,XBOOLE_0:def 5; end; then A19: rng q c=dom f2\{lim_left(f1,x0)}; rng(f1/*s)c=dom f2 by A8,Th1; then A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27 .=((f2*f1)/*s)^\k by A11,VALUED_0:31; A21: rng s c=dom f1/\left_open_halfline(x0) by A8,Th1; then A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 7; lim(f1/*s)=lim_left(f1,x0) by A1,A7,A21,LIMFUNC2:def 7; then A23: lim q=lim_left(f1,x0) by A22,SEQ_4:20; lim(f2,lim_left(f1,x0))=lim(f2,lim_left(f1,x0)); then A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC3:def 4; hence (f2*f1)/*s is convergent by A20,SEQ_4:21; lim(f2/*q)=lim(f2,lim_left(f1,x0)) by A2,A22,A23,A19,LIMFUNC3:def 4; hence lim((f2*f1)/*s)=lim(f2,lim_left(f1,x0)) by A24,A20,SEQ_4:22; end; hence f2*f1 is_left_convergent_in x0 by A3,LIMFUNC2:def 1; hence thesis by A6,LIMFUNC2:def 7; end; theorem f1 is_convergent_in x0 & f2 is_right_convergent_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0) by A5; then f1.(s.(n+k)) in {g2: lim(f1,x0)lim_right(f1,x0)) implies f2*f1 is_right_convergent_in x0 & lim_right(f2*f1,x0)=lim(f2,lim_right(f1,x0)) proof assume that A1: f1 is_right_convergent_in x0 and A2: f2 is_convergent_in lim_right(f1,x0) and A3: for r st x0lim_right(f1,x0); A6: now let s be Real_Sequence; assume that A7: s is convergent & lim s=x0 and A8: rng s c=dom(f2*f1)/\right_open_halfline(x0); consider k being Nat such that A9: for n being Nat st k<=n holds s.nlim_right(f1,x0) by A5; then A18: not f1.(s.(n+k)) in {lim_right(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11; hence x in dom f2\{lim_right(f1,x0)} by A18,A15,XBOOLE_0:def 5; end; then A19: rng q c=dom f2\{lim_right(f1,x0)}; rng(f1/*s)c=dom f2 by A8,Th1; then A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27 .=((f2*f1)/*s)^\k by A11,VALUED_0:31; A21: rng s c=dom f1/\right_open_halfline(x0) by A8,Th1; then A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 8; lim(f1/*s)=lim_right(f1,x0) by A1,A7,A21,LIMFUNC2:def 8; then A23: lim q=lim_right(f1,x0) by A22,SEQ_4:20; lim(f2,lim_right(f1,x0))=lim(f2,lim_right(f1,x0)); then A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC3:def 4; hence (f2*f1)/*s is convergent by A20,SEQ_4:21; lim(f2/*q)=lim(f2,lim_right(f1,x0)) by A2,A22,A23,A19,LIMFUNC3:def 4; hence lim((f2*f1)/*s)=lim(f2,lim_right(f1,x0)) by A24,A20,SEQ_4:22; end; hence f2*f1 is_right_convergent_in x0 by A3,LIMFUNC2:def 4; hence thesis by A6,LIMFUNC2:def 8; end; theorem f1 is_convergent_in x0 & f2 is_convergent_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0)) implies f2*f1 is_convergent_in x0 & lim(f2*f1, x0)=lim(f2,lim(f1,x0)) proof assume that A1: f1 is_convergent_in x0 and A2: f2 is_convergent_in lim(f1,x0) and A3: for r1,r2 st r1lim(f1, x0); A6: now let s be Real_Sequence; assume that A7: s is convergent & lim s=x0 and A8: rng s c=dom(f2*f1)\{x0}; consider k being Element of NAT such that A9: for n being Element of NAT st k<=n holds x0-glim(f1,x0) by A5; then A16: not f1.(s.(n+k)) in {lim(f1,x0)} by TARSKI:def 1; f1.(s.(n+k)) in dom f2 by A10,A15,FUNCT_1:11; hence x in dom f2\{lim(f1,x0)} by A16,A13,XBOOLE_0:def 5; end; then A17: rng q c=dom f2\{lim(f1,x0)}; rng(f1/*s)c=dom f2 by A8,Th2; then A18: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27 .=((f2*f1)/*s)^\k by A10,VALUED_0:31; A19: rng s c=dom f1\{x0} by A8,Th2; then A20: f1/*s is convergent by A1,A2,A7,LIMFUNC3:def 4; lim(f1/*s)=lim(f1,x0) by A1,A7,A19,LIMFUNC3:def 4; then A21: lim q=lim(f1,x0) by A20,SEQ_4:20; lim(f2,lim(f1,x0))=lim(f2,lim(f1,x0)); then A22: f2/*q is convergent by A2,A20,A21,A17,LIMFUNC3:def 4; hence (f2*f1)/*s is convergent by A18,SEQ_4:21; lim(f2/*q)=lim(f2,lim(f1,x0)) by A2,A20,A21,A17,LIMFUNC3:def 4; hence lim((f2*f1)/*s)=lim(f2,lim(f1,x0)) by A22,A18,SEQ_4:22; end; hence f2*f1 is_convergent_in x0 by A3,LIMFUNC3:def 1; hence thesis by A6,LIMFUNC3:def 4; end;