deffunc H_{1}( Nat) -> set = (tau to_power $1) / (sqrt 5);

let F be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) implies ( F is convergent & lim F = tau ) )

consider f being Real_Sequence such that

A1: for n being Nat holds f . n = Fib n from SEQ_1:sch 1();

set f2 = f ^\ 2;

set f1 = f ^\ 1;

A2: (f ^\ 1) ^\ 1 = f ^\ (1 + 1) by NAT_1:48

.= f ^\ 2 ;

A3: for n being Element of NAT holds (f ^\ 2) . n <> 0

A4: for n being Nat holds ((f ^\ 2) /" (f ^\ 2)) . n = jj

A7: (f /" f) ^\ 2 = (f ^\ 2) /" (f ^\ 2) by SEQM_3:20;

then A8: f /" f is convergent by A6, SEQ_4:21;

((f ^\ 2) /" (f ^\ 2)) . 0 = 1 by A4;

then lim ((f ^\ 2) /" (f ^\ 2)) = 1 by A6, SEQ_4:25;

then A9: lim (f /" f) = 1 by A6, A7, SEQ_4:22;

ex g being Real_Sequence st

for n being Nat holds g . n = H_{1}(n)
from SEQ_1:sch 1();

then consider g being Real_Sequence such that

A10: for n being Nat holds g . n = H_{1}(n)
;

set g1 = g ^\ 1;

A11: for n being Nat holds g . n <> 0

A15: (f ^\ 2) /" (f ^\ 1) = ((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1)) by Th9, A14;

set g2 = (g ^\ 1) ^\ 1;

for n being Nat holds (f ^\ 1) . n <> 0

for n being Nat holds (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0

(g ^\ 1) ^\ 1 = g ^\ (1 + 1) by NAT_1:48;

then A22: ((g ^\ 1) ^\ 1) /" (f ^\ 2) = (g /" f) ^\ 2 by SEQM_3:20;

A23: for n being Element of NAT holds (f ^\ 1) . n = Fib (n + 1)

for n being Element of NAT holds F . n = ((f ^\ 1) /" f) . n

then A25: (f ^\ 2) /" (f ^\ 1) = F ^\ 1 by A2, SEQM_3:20;

A26: ((g ^\ 1) ^\ 1) /" (g ^\ 1) = ((g ^\ 1) /" g) ^\ 1 by SEQM_3:20;

A27: for n being Nat holds ((g ^\ 1) /" g) . n = tau

then A31: (g ^\ 1) /" g is constant by A27, VALUED_0:def 18;

A32: for x being Real st 0 < x holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x

then A42: lim (f ") = 0 by A32, SEQ_2:def 7;

deffunc H_{2}( Nat) -> set = (tau_bar to_power $1) / (sqrt 5);

ex h being Real_Sequence st

for n being Nat holds h . n = H_{2}(n)
from SEQ_1:sch 1();

then consider h being Real_Sequence such that

A43: for n being Nat holds h . n = H_{2}(n)
;

A44: for n being Element of NAT holds f . n = (g . n) - (h . n)

then A46: g /" f = (f /" f) + (h /" f) by SEQ_1:49;

for n being Nat holds |.(h . n).| < 1

f " is convergent by A32, SEQ_2:def 6;

then A49: h /" f is convergent by A48, A42, SEQ_2:25;

then A50: g /" f is convergent by A8, A46;

((g ^\ 1) /" g) . 0 = tau by A27;

then lim ((g ^\ 1) /" g) = tau by A31, SEQ_4:25;

then A51: lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau by A31, A26, SEQ_4:20;

A52: (g ^\ 1) /" (f ^\ 1) = (g /" f) ^\ 1 by SEQM_3:20;

lim (h /" f) = 0 by A48, A41, A42, SEQ_2:26;

then A53: lim (g /" f) = 1 + 0 by A49, A8, A9, A46, SEQ_2:6

.= 1 ;

then A54: lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) = 1 by A50, A22, SEQ_4:20;

then (((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is convergent by A50, A22, A21, SEQ_2:21;

then A55: (f ^\ 2) /" ((g ^\ 1) ^\ 1) is convergent by SEQ_1:40;

A56: (f ^\ 2) /" (g ^\ 1) = ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) (#) (((g ^\ 1) ^\ 1) /" (g ^\ 1)) by A14, Th9;

then A57: (f ^\ 2) /" (g ^\ 1) is convergent by A31, A55, A26;

then A58: (f ^\ 2) /" (f ^\ 1) is convergent by A50, A52, A15;

hence F is convergent by A25, SEQ_4:21; :: thesis: lim F = tau

lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) ") = 1 " by A50, A22, A54, A21, SEQ_2:22

.= 1 ;

then lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1 by SEQ_1:40;

then A59: lim ((f ^\ 2) /" (g ^\ 1)) = 1 * tau by A31, A56, A55, A26, A51, SEQ_2:15

.= tau ;

lim ((g ^\ 1) /" (f ^\ 1)) = 1 by A50, A53, A52, SEQ_4:20;

then lim ((f ^\ 2) /" (f ^\ 1)) = tau * 1 by A50, A59, A57, A52, A15, SEQ_2:15;

hence lim F = tau by A58, A25, SEQ_4:22; :: thesis: verum

let F be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) implies ( F is convergent & lim F = tau ) )

consider f being Real_Sequence such that

A1: for n being Nat holds f . n = Fib n from SEQ_1:sch 1();

set f2 = f ^\ 2;

set f1 = f ^\ 1;

A2: (f ^\ 1) ^\ 1 = f ^\ (1 + 1) by NAT_1:48

.= f ^\ 2 ;

A3: for n being Element of NAT holds (f ^\ 2) . n <> 0

proof

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
let n be Element of NAT ; :: thesis: (f ^\ 2) . n <> 0

(f ^\ 2) . n = f . (n + 2) by NAT_1:def 3

.= Fib ((n + 1) + 1) by A1 ;

hence (f ^\ 2) . n <> 0 by Lm3; :: thesis: verum

end;(f ^\ 2) . n = f . (n + 2) by NAT_1:def 3

.= Fib ((n + 1) + 1) by A1 ;

hence (f ^\ 2) . n <> 0 by Lm3; :: thesis: verum

A4: for n being Nat holds ((f ^\ 2) /" (f ^\ 2)) . n = jj

proof

then A6:
(f ^\ 2) /" (f ^\ 2) is constant
by VALUED_0:def 18;
let n be Nat; :: thesis: ((f ^\ 2) /" (f ^\ 2)) . n = jj

A5: n in NAT by ORDINAL1:def 12;

then ((f ^\ 2) /" (f ^\ 2)) . n = ((f ^\ 2) . n) * (((f ^\ 2) . n) ") by Th10

.= ((f ^\ 2) . n) * (1 / ((f ^\ 2) . n))

.= 1 by A3, A5, XCMPLX_1:106 ;

hence ((f ^\ 2) /" (f ^\ 2)) . n = jj ; :: thesis: verum

end;A5: n in NAT by ORDINAL1:def 12;

then ((f ^\ 2) /" (f ^\ 2)) . n = ((f ^\ 2) . n) * (((f ^\ 2) . n) ") by Th10

.= ((f ^\ 2) . n) * (1 / ((f ^\ 2) . n))

.= 1 by A3, A5, XCMPLX_1:106 ;

hence ((f ^\ 2) /" (f ^\ 2)) . n = jj ; :: thesis: verum

A7: (f /" f) ^\ 2 = (f ^\ 2) /" (f ^\ 2) by SEQM_3:20;

then A8: f /" f is convergent by A6, SEQ_4:21;

((f ^\ 2) /" (f ^\ 2)) . 0 = 1 by A4;

then lim ((f ^\ 2) /" (f ^\ 2)) = 1 by A6, SEQ_4:25;

then A9: lim (f /" f) = 1 by A6, A7, SEQ_4:22;

ex g being Real_Sequence st

for n being Nat holds g . n = H

then consider g being Real_Sequence such that

A10: for n being Nat holds g . n = H

set g1 = g ^\ 1;

A11: for n being Nat holds g . n <> 0

proof

then A14:
g is non-zero
by SEQ_1:5;
let n be Nat; :: thesis: g . n <> 0

A12: (sqrt 5) " <> 0 by SQUARE_1:20, SQUARE_1:27, XCMPLX_1:202;

A13: tau |^ n <> 0 by Lm12, PREPOWER:5;

g . n = (tau to_power n) / (sqrt 5) by A10

.= (tau to_power n) * ((sqrt 5) ")

.= (tau |^ n) * ((sqrt 5) ") by POWER:41 ;

hence g . n <> 0 by A13, A12, XCMPLX_1:6; :: thesis: verum

end;A12: (sqrt 5) " <> 0 by SQUARE_1:20, SQUARE_1:27, XCMPLX_1:202;

A13: tau |^ n <> 0 by Lm12, PREPOWER:5;

g . n = (tau to_power n) / (sqrt 5) by A10

.= (tau to_power n) * ((sqrt 5) ")

.= (tau |^ n) * ((sqrt 5) ") by POWER:41 ;

hence g . n <> 0 by A13, A12, XCMPLX_1:6; :: thesis: verum

A15: (f ^\ 2) /" (f ^\ 1) = ((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1)) by Th9, A14;

set g2 = (g ^\ 1) ^\ 1;

for n being Nat holds (f ^\ 1) . n <> 0

proof

then A17:
f ^\ 1 is non-zero
by SEQ_1:5;
let n be Nat; :: thesis: (f ^\ 1) . n <> 0

A16: n in NAT by ORDINAL1:def 12;

(f ^\ 1) . n = f . (n + 1) by NAT_1:def 3

.= Fib (n + 1) by A1 ;

hence (f ^\ 1) . n <> 0 by Lm6, A16; :: thesis: verum

end;A16: n in NAT by ORDINAL1:def 12;

(f ^\ 1) . n = f . (n + 1) by NAT_1:def 3

.= Fib (n + 1) by A1 ;

hence (f ^\ 1) . n <> 0 by Lm6, A16; :: thesis: verum

for n being Nat holds (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0

proof

then A21:
((g ^\ 1) ^\ 1) /" (f ^\ 2) is non-zero
by SEQ_1:5;
let n be Nat; :: thesis: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0

A18: n in NAT by ORDINAL1:def 12;

A19: ((g ^\ 1) ^\ 1) . n <> 0 by A14, SEQ_1:5;

A20: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n = (((g ^\ 1) ^\ 1) . n) * (((f ^\ 2) . n) ") by Th10, A18;

((f ^\ 2) . n) " <> 0 by A17, A2, SEQ_1:5, XCMPLX_1:202;

hence (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 by A19, A20, XCMPLX_1:6; :: thesis: verum

end;A18: n in NAT by ORDINAL1:def 12;

A19: ((g ^\ 1) ^\ 1) . n <> 0 by A14, SEQ_1:5;

A20: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n = (((g ^\ 1) ^\ 1) . n) * (((f ^\ 2) . n) ") by Th10, A18;

((f ^\ 2) . n) " <> 0 by A17, A2, SEQ_1:5, XCMPLX_1:202;

hence (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 by A19, A20, XCMPLX_1:6; :: thesis: verum

(g ^\ 1) ^\ 1 = g ^\ (1 + 1) by NAT_1:48;

then A22: ((g ^\ 1) ^\ 1) /" (f ^\ 2) = (g /" f) ^\ 2 by SEQM_3:20;

A23: for n being Element of NAT holds (f ^\ 1) . n = Fib (n + 1)

proof

assume A24:
for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n)
; :: thesis: ( F is convergent & lim F = tau )
let n be Element of NAT ; :: thesis: (f ^\ 1) . n = Fib (n + 1)

(f ^\ 1) . n = f . (n + 1) by NAT_1:def 3

.= Fib (n + 1) by A1 ;

hence (f ^\ 1) . n = Fib (n + 1) ; :: thesis: verum

end;(f ^\ 1) . n = f . (n + 1) by NAT_1:def 3

.= Fib (n + 1) by A1 ;

hence (f ^\ 1) . n = Fib (n + 1) ; :: thesis: verum

for n being Element of NAT holds F . n = ((f ^\ 1) /" f) . n

proof

then
F = (f ^\ 1) /" f
by FUNCT_2:63;
let n be Element of NAT ; :: thesis: F . n = ((f ^\ 1) /" f) . n

((f ^\ 1) /" f) . n = ((f ^\ 1) . n) / (f . n) by Th10

.= (Fib (n + 1)) / (f . n) by A23

.= (Fib (n + 1)) / (Fib n) by A1 ;

hence F . n = ((f ^\ 1) /" f) . n by A24; :: thesis: verum

end;((f ^\ 1) /" f) . n = ((f ^\ 1) . n) / (f . n) by Th10

.= (Fib (n + 1)) / (f . n) by A23

.= (Fib (n + 1)) / (Fib n) by A1 ;

hence F . n = ((f ^\ 1) /" f) . n by A24; :: thesis: verum

then A25: (f ^\ 2) /" (f ^\ 1) = F ^\ 1 by A2, SEQM_3:20;

A26: ((g ^\ 1) ^\ 1) /" (g ^\ 1) = ((g ^\ 1) /" g) ^\ 1 by SEQM_3:20;

A27: for n being Nat holds ((g ^\ 1) /" g) . n = tau

proof

tau in REAL
by XREAL_0:def 1;
let n be Nat; :: thesis: ((g ^\ 1) /" g) . n = tau

A28: n in NAT by ORDINAL1:def 12;

A29: g . n = (tau to_power n) / (sqrt 5) by A10

.= (tau to_power n) * ((sqrt 5) ")

.= (tau |^ n) * ((sqrt 5) ") by POWER:41 ;

A30: g . n <> 0 by A11;

(g ^\ 1) . n = g . (n + 1) by NAT_1:def 3

.= (tau to_power (n + 1)) / (sqrt 5) by A10

.= (tau to_power (n + 1)) * ((sqrt 5) ")

.= (tau |^ (n + 1)) * ((sqrt 5) ") by POWER:41

.= (tau * (tau |^ n)) * ((sqrt 5) ") by NEWTON:6

.= tau * (g . n) by A29 ;

then ((g ^\ 1) /" g) . n = (tau * (g . n)) * ((g . n) ") by A28, Th10

.= tau * ((g . n) * ((g . n) "))

.= tau * 1 by A30, XCMPLX_0:def 7

.= tau ;

hence ((g ^\ 1) /" g) . n = tau ; :: thesis: verum

end;A28: n in NAT by ORDINAL1:def 12;

A29: g . n = (tau to_power n) / (sqrt 5) by A10

.= (tau to_power n) * ((sqrt 5) ")

.= (tau |^ n) * ((sqrt 5) ") by POWER:41 ;

A30: g . n <> 0 by A11;

(g ^\ 1) . n = g . (n + 1) by NAT_1:def 3

.= (tau to_power (n + 1)) / (sqrt 5) by A10

.= (tau to_power (n + 1)) * ((sqrt 5) ")

.= (tau |^ (n + 1)) * ((sqrt 5) ") by POWER:41

.= (tau * (tau |^ n)) * ((sqrt 5) ") by NEWTON:6

.= tau * (g . n) by A29 ;

then ((g ^\ 1) /" g) . n = (tau * (g . n)) * ((g . n) ") by A28, Th10

.= tau * ((g . n) * ((g . n) "))

.= tau * 1 by A30, XCMPLX_0:def 7

.= tau ;

hence ((g ^\ 1) /" g) . n = tau ; :: thesis: verum

then A31: (g ^\ 1) /" g is constant by A27, VALUED_0:def 18;

A32: for x being Real st 0 < x holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x

proof

then A41:
f " is convergent
by SEQ_2:def 6;
let x be Real; :: thesis: ( 0 < x implies ex n being Nat st

for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x )

assume 0 < x ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x

then consider k being Element of NAT such that

A33: k > 0 and

0 < 1 / k and

A34: 1 / k <= x by Th3;

for m being Nat st k + 2 <= m holds

|.(((f ") . m) - 0).| < x

for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x ; :: thesis: verum

end;for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x )

assume 0 < x ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x

then consider k being Element of NAT such that

A33: k > 0 and

0 < 1 / k and

A34: 1 / k <= x by Th3;

for m being Nat st k + 2 <= m holds

|.(((f ") . m) - 0).| < x

proof

hence
ex n being Nat st
let m be Nat; :: thesis: ( k + 2 <= m implies |.(((f ") . m) - 0).| < x )

A35: m in NAT by ORDINAL1:def 12;

k + 2 = (k + 1) + 1 ;

then A36: Fib (k + 2) >= k + 1 by Lm3;

assume k + 2 <= m ; :: thesis: |.(((f ") . m) - 0).| < x

then Fib (k + 2) <= Fib m by Lm5, A35;

then k + 1 <= Fib m by A36, XXREAL_0:2;

then A37: k + 1 <= f . m by A1;

then 0 < f . m ;

then A38: 0 <= (f . m) " ;

k + 0 < k + 1 by XREAL_1:6;

then A39: 1 / (k + 1) < 1 / k by A33, XREAL_1:88;

A40: |.(((f ") . m) - 0).| = |.((f . m) ").| by VALUED_1:10

.= (f . m) " by A38, ABSVALUE:def 1

.= 1 / (f . m) ;

1 / (f . m) <= 1 / (k + 1) by A37, XREAL_1:85;

then 1 / (f . m) < 1 / k by A39, XXREAL_0:2;

hence |.(((f ") . m) - 0).| < x by A34, A40, XXREAL_0:2; :: thesis: verum

end;A35: m in NAT by ORDINAL1:def 12;

k + 2 = (k + 1) + 1 ;

then A36: Fib (k + 2) >= k + 1 by Lm3;

assume k + 2 <= m ; :: thesis: |.(((f ") . m) - 0).| < x

then Fib (k + 2) <= Fib m by Lm5, A35;

then k + 1 <= Fib m by A36, XXREAL_0:2;

then A37: k + 1 <= f . m by A1;

then 0 < f . m ;

then A38: 0 <= (f . m) " ;

k + 0 < k + 1 by XREAL_1:6;

then A39: 1 / (k + 1) < 1 / k by A33, XREAL_1:88;

A40: |.(((f ") . m) - 0).| = |.((f . m) ").| by VALUED_1:10

.= (f . m) " by A38, ABSVALUE:def 1

.= 1 / (f . m) ;

1 / (f . m) <= 1 / (k + 1) by A37, XREAL_1:85;

then 1 / (f . m) < 1 / k by A39, XXREAL_0:2;

hence |.(((f ") . m) - 0).| < x by A34, A40, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

|.(((f ") . m) - 0).| < x ; :: thesis: verum

then A42: lim (f ") = 0 by A32, SEQ_2:def 7;

deffunc H

ex h being Real_Sequence st

for n being Nat holds h . n = H

then consider h being Real_Sequence such that

A43: for n being Nat holds h . n = H

A44: for n being Element of NAT holds f . n = (g . n) - (h . n)

proof

for n being Nat holds g . n = (f . n) + (h . n)
let n be Element of NAT ; :: thesis: f . n = (g . n) - (h . n)

f . n = Fib n by A1

.= ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7

.= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5))

.= (g . n) - ((tau_bar to_power n) / (sqrt 5)) by A10

.= (g . n) - (h . n) by A43 ;

hence f . n = (g . n) - (h . n) ; :: thesis: verum

end;f . n = Fib n by A1

.= ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7

.= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5))

.= (g . n) - ((tau_bar to_power n) / (sqrt 5)) by A10

.= (g . n) - (h . n) by A43 ;

hence f . n = (g . n) - (h . n) ; :: thesis: verum

proof

then
g = f + h
by SEQ_1:7;
let n be Nat; :: thesis: g . n = (f . n) + (h . n)

A45: n in NAT by ORDINAL1:def 12;

f . n = (g . n) - (h . n) by A44, A45;

hence g . n = (f . n) + (h . n) ; :: thesis: verum

end;A45: n in NAT by ORDINAL1:def 12;

f . n = (g . n) - (h . n) by A44, A45;

hence g . n = (f . n) + (h . n) ; :: thesis: verum

then A46: g /" f = (f /" f) + (h /" f) by SEQ_1:49;

for n being Nat holds |.(h . n).| < 1

proof

then A48:
h is bounded
by SEQ_2:3;
let n be Nat; :: thesis: |.(h . n).| < 1

A47: n in NAT by ORDINAL1:def 12;

h . n = (tau_bar to_power n) / (sqrt 5) by A43;

hence |.(h . n).| < 1 by Lm16, A47; :: thesis: verum

end;A47: n in NAT by ORDINAL1:def 12;

h . n = (tau_bar to_power n) / (sqrt 5) by A43;

hence |.(h . n).| < 1 by Lm16, A47; :: thesis: verum

f " is convergent by A32, SEQ_2:def 6;

then A49: h /" f is convergent by A48, A42, SEQ_2:25;

then A50: g /" f is convergent by A8, A46;

((g ^\ 1) /" g) . 0 = tau by A27;

then lim ((g ^\ 1) /" g) = tau by A31, SEQ_4:25;

then A51: lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau by A31, A26, SEQ_4:20;

A52: (g ^\ 1) /" (f ^\ 1) = (g /" f) ^\ 1 by SEQM_3:20;

lim (h /" f) = 0 by A48, A41, A42, SEQ_2:26;

then A53: lim (g /" f) = 1 + 0 by A49, A8, A9, A46, SEQ_2:6

.= 1 ;

then A54: lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) = 1 by A50, A22, SEQ_4:20;

then (((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is convergent by A50, A22, A21, SEQ_2:21;

then A55: (f ^\ 2) /" ((g ^\ 1) ^\ 1) is convergent by SEQ_1:40;

A56: (f ^\ 2) /" (g ^\ 1) = ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) (#) (((g ^\ 1) ^\ 1) /" (g ^\ 1)) by A14, Th9;

then A57: (f ^\ 2) /" (g ^\ 1) is convergent by A31, A55, A26;

then A58: (f ^\ 2) /" (f ^\ 1) is convergent by A50, A52, A15;

hence F is convergent by A25, SEQ_4:21; :: thesis: lim F = tau

lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) ") = 1 " by A50, A22, A54, A21, SEQ_2:22

.= 1 ;

then lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1 by SEQ_1:40;

then A59: lim ((f ^\ 2) /" (g ^\ 1)) = 1 * tau by A31, A56, A55, A26, A51, SEQ_2:15

.= tau ;

lim ((g ^\ 1) /" (f ^\ 1)) = 1 by A50, A53, A52, SEQ_4:20;

then lim ((f ^\ 2) /" (f ^\ 1)) = tau * 1 by A50, A59, A57, A52, A15, SEQ_2:15;

hence lim F = tau by A58, A25, SEQ_4:22; :: thesis: verum