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

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

let 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;

hence s1 = s2 ; :: thesis: verum