let s1, s2 be Complex_Sequence; :: thesis: ( ( for n being Nat holds s1 . n = (z |^ (n + 1)) / ((n + 2) !) ) & ( for n being Nat holds s2 . n = (z |^ (n + 1)) / ((n + 2) !) ) implies s1 = s2 )
assume that
A1: for x being Nat holds s1 . x = H₂(x) and
A2: 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 A1
.= s2 . x by A2 ; :: thesis: verum