let seq be Complex_Sequence; :: thesis: for h1, h2 being PartFunc of COMPLEX,COMPLEX 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 COMPLEX,COMPLEX; :: thesis: ( 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 ) ; :: thesis: ( (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) = COMPLEX by PARTFUN1:def 2;
then (dom h1) /\ (dom h2) = COMPLEX by VALUED_1:def 1;
then A1: rng seq c= (dom h1) /\ (dom h2) ;
hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by Th7; :: thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, Th7; :: thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
thus (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by A1, Th7; :: thesis: verum