reconsider r1 = r as Element of REAL by XREAL_0:def 1;
A1:
for n being Nat
for x being Element of REAL ex y being Element of REAL st S1[n,x,y]
proof
let n be
Nat;
for x being Element of REAL ex y being Element of REAL st S1[n,x,y]let x be
Element of
REAL ;
ex y being Element of REAL st S1[n,x,y]
consider y being
Real such that A2:
S1[
n,
x,
y]
;
reconsider y =
y as
Element of
REAL by XREAL_0:def 1;
take
y
;
S1[n,x,y]
thus
S1[
n,
x,
y]
by A2;
verum
end;
consider f being sequence of REAL such that
A3:
f . 0 = r1
and
A4:
for n being Nat holds S1[n,f . n,f . (n + 1)]
from RECDEF_1:sch 2(A1);
take
f
; ( f . 0 = r & ( for n being Nat holds f . (n + 1) = 1 / (frac (f . n)) ) )
thus
f . 0 = r
by A3; for n being Nat holds f . (n + 1) = 1 / (frac (f . n))
let n be Nat; f . (n + 1) = 1 / (frac (f . n))
thus
f . (n + 1) = 1 / (frac (f . n))
by A4; verum