let s1, s2 be Real_Sequence; :: thesis: ( ( for x being Nat holds s1 . x = Sum (c (#) (seq_a^ (x,1,0))) ) & ( for x being Nat holds s2 . x = Sum (c (#) (seq_a^ (x,1,0))) ) implies s1 = s2 )

assume that

A1: for x being Nat holds s1 . x = Sum (c (#) (seq_a^ (x,1,0))) and

A2: for x being Nat holds s2 . x = Sum (c (#) (seq_a^ (x,1,0))) ; :: thesis: s1 = s2

assume that

A1: for x being Nat holds s1 . x = Sum (c (#) (seq_a^ (x,1,0))) and

A2: for x being Nat holds s2 . x = Sum (c (#) (seq_a^ (x,1,0))) ; :: thesis: s1 = s2

now :: thesis: for x being Element of NAT holds s1 . x = s2 . x

hence
s1 = s2
; :: thesis: verumlet x be Element of NAT ; :: thesis: s1 . x = s2 . x

thus s1 . x = Sum (c (#) (seq_a^ (x,1,0))) by A1

.= s2 . x by A2 ; :: thesis: verum

end;thus s1 . x = Sum (c (#) (seq_a^ (x,1,0))) by A1

.= s2 . x by A2 ; :: thesis: verum