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 S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of REAL ex y being Element of REAL st S₁[n,x,y]
let x be Element of REAL ; :: thesis: ex y being Element of REAL st S₁[n,x,y]
consider y being Real such that
A2: S₁[n,x,y] ;
reconsider y = y as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by A2; :: thesis: verum

end;

consider f being sequence of REAL such that
A3: f . 0 = r1 and
A4: for n being Nat holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A1);
take f ; :: thesis: ( f . 0 = r & ( for n being Nat holds f . (n + 1) = 1 / (frac (f . n)) ) )
thus f . 0 = r by A3; :: thesis: for n being Nat holds f . (n + 1) = 1 / (frac (f . n))
let n be Nat; :: thesis: f . (n + 1) = 1 / (frac (f . n))
thus f . (n + 1) = 1 / (frac (f . n)) by A4; :: thesis: verum