reconsider r1 = r as Element of REAL by XREAL_0:def 1;
A1: for n being Element of NAT
for x being Element of REAL ex y being Element of REAL st S₁[n,x,y] ;
consider f being Function of NAT ,REAL such that
A2: f . 0 = r1 and
A3: for n being Element of 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 A2; :: 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))
n in NAT by ORDINAL1:def 13;
hence f . (n + 1) = 1 / (frac (f . n)) by A3; :: thesis: verum