theorem Th23: :: NAGATA_1:23

for T being non empty TopSpace
for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds
( ADD is having_a_unity & ADD is commutative & ADD is associative )