let C1, C2 be complex-valued Function; :: thesis: ( dom C1 = dom f & ( for x being set holds C1 . x = Sum (f . x) ) & dom C2 = dom f & ( for x being set holds C2 . x = Sum (f . x) ) implies C1 = C2 )
assume that
A5: ( dom C1 = dom f & ( for x being set holds C1 . x = Sum (f . x) ) ) and
A6: ( dom C2 = dom f & ( for x being set holds C2 . x = Sum (f . x) ) ) ; :: thesis: C1 = C2

now :: thesis: for x being object holds C1 . x = C2 . x

let x be object ; :: thesis: C1 . x = C2 . x
reconsider X = x as set by TARSKI:1;
thus C1 . x = Sum (f . X) by A5
.= C2 . x by A6 ; :: thesis: verum

end;

hence C1 = C2 by A5, A6; :: thesis: verum