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
A4: g1 . 0 = r and
A5: for n being Nat holds g1 . (n + 1) = 1 / (frac (g1 . n)) and
A6: g2 . 0 = r and
A7: for n being Nat holds g2 . (n + 1) = 1 / (frac (g2 . n)) ; :: thesis: g1 = g2
reconsider r1 = r as Element of REAL by XREAL_0:def 1;
A8: for n being Nat
for x, y1, y2 being Element of REAL st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
A9: g1 . 0 = r1 by A4;
B9: for n being Nat holds S₁[n,g1 . n,g1 . (n + 1)] by A5;
A10: g2 . 0 = r1 by A6;
B10: for n being Nat holds S₁[n,g2 . n,g2 . (n + 1)] by A7;
thus g1 = g2 from NAT_1:sch 14(A9, B9, A10, B10, A8); :: thesis: verum