let s1, s2 be Complex_Sequence; :: thesis: ( ( for n being Nat holds s1 . n = (z |^ n) / ((n + 2) !) ) & ( for n being Nat holds s2 . n = (z |^ n) / ((n + 2) !) ) 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