let W be 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) )
let h1, h2 be 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) )
let seq be sequence of W; ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) )
assume
( h1 is total & h2 is total )
; ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
then
dom (h1 + h2) = W
by PARTFUN1:def 2;
then
(dom h1) /\ (dom h2) = W
by VALUED_1:def 1;
then A1:
rng seq c= (dom h1) /\ (dom h2)
;
hence
(h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq)
by Th8; ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
thus
(h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)
by A1, Th8; (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
thus
(h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
by A1, Th8; verum