let s1, s2 be Real_Sequence; :: thesis: ( s1 . 0 = (scf r) . 0 & ( for n being Nat holds s1 . (n + 1) = (1 / (s1 . n)) + ((scf r) . (n + 1)) ) & s2 . 0 = (scf r) . 0 & ( for n being Nat holds s2 . (n + 1) = (1 / (s2 . n)) + ((scf r) . (n + 1)) ) implies s1 = s2 )
assume that
A3: s1 . 0 = (scf r) . 0 and
A4: for n being Nat holds s1 . (n + 1) = (1 / (s1 . n)) + ((scf r) . (n + 1)) and
A5: s2 . 0 = (scf r) . 0 and
A6: for n being Nat holds s2 . (n + 1) = (1 / (s2 . n)) + ((scf r) . (n + 1)) ; :: thesis: s1 = s2
defpred S₂[ Nat] means s1 . $1 = s2 . $1;
A7: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume s1 . k = s2 . k ; :: thesis: S₂[k + 1]
hence s1 . (k + 1) = (1 / (s2 . k)) + ((scf r) . (k + 1)) by A4
.= s2 . (k + 1) by A6 ;
:: thesis: verum

end;

let x be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: s1 . x = s2 . x
A8: S₂[ 0 ] by A3, A5;
for n being Nat holds S₂[n] from NAT_1:sch 2(A8, A7);
hence s1 . x = s2 . x ; :: thesis: verum