for i being Element of NAT
for f, g being PartFunc of (REAL i),REAL holds
( <>* (f + g) = (<>* f) + (<>* g) & <>* (f - g) = (<>* f) - (<>* g) )