theorem :: RFUNCT_2:13

for W being non empty set
for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )