let s1, s2 be Real_Sequence; :: thesis: ( ( for n being Nat holds s1 . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) ) & ( for n being Nat holds s2 . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) ) implies s1 = s2 )
assume that
A3: for x being Nat holds s1 . x = H₂(x) and
A4: for x being Nat holds s2 . x = H₂(x) ; :: thesis: s1 = s2
let x be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: s1 . x = s2 . x
thus s1 . x = H₂(x) by A3
.= s2 . x by A4 ; :: thesis: verum