A4: for n being Nat
for x, y1, y2 being Element of REAL st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
reconsider r1 = r as Element of REAL by XREAL_0:def 1;
let g1, g2 be Real_Sequence; :: thesis: ( g1 . 0 = r & ( for n being Nat holds g1 . (n + 1) = 1 / (frac (g1 . n)) ) & g2 . 0 = r & ( for n being Nat holds g2 . (n + 1) = 1 / (frac (g2 . n)) ) implies g1 = g2 )
assume that
A5: g1 . 0 = r and
A6: for n being Nat holds g1 . (n + 1) = 1 / (frac (g1 . n)) and
A7: g2 . 0 = r and
A8: for n being Nat holds g2 . (n + 1) = 1 / (frac (g2 . n)) ; :: thesis: g1 = g2
A9: for n being Nat holds S₁[n,g1 . n,g1 . (n + 1)] by A6;
A10: for n being Nat holds S₁[n,g2 . n,g2 . (n + 1)] by A8;
A11: g2 . 0 = r1 by A7;
A12: g1 . 0 = r1 by A5;
thus g1 = g2 from NAT_1:sch 14(A12, A9, A11, A10, A4); :: thesis: verum