let f1, f2 be Real_Sequence; :: thesis: ( ( for d being Nat holds f1 . d = Sum ((- (s . d)) rExpSeq) ) & ( for d being Nat holds f2 . d = Sum ((- (s . d)) rExpSeq) ) implies f1 = f2 )
assume that
A2: for d being Nat holds f1 . d = Sum ((- (s . d)) rExpSeq) and
A3: for d being Nat holds f2 . d = Sum ((- (s . d)) rExpSeq) ; :: thesis: f1 = f2
let d be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: f1 . d = f2 . d
f1 . d = Sum ((- (s . d)) rExpSeq) by A2;
hence f1 . d = f2 . d by A3; :: thesis: verum