A5: 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
A6: g1 . 0 = r and
A7: for n being Nat holds g1 . (n + 1) = 1 / (frac (g1 . n)) and
A8: g2 . 0 = r and
A9: for n being Nat holds g2 . (n + 1) = 1 / (frac (g2 . n)) ; :: thesis: g1 = g2
A10: for n being Nat holds S₁[n,g1 . n,g1 . (n + 1)] by A7;
A11: for n being Nat holds S₁[n,g2 . n,g2 . (n + 1)] by A9;
A12: g2 . 0 = r1 by A8;
A13: g1 . 0 = r1 by A6;
thus g1 = g2 from NAT_1:sch 14(A13, A10, A12, A11, A5); :: thesis: verum