let S, T be RealNormSpace; :: thesis: for h1, h2 being PartFunc of S,T

for seq being sequence of S st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

let h1, h2 be PartFunc of S,T; :: thesis: for seq being sequence of S st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

let seq be sequence of S; :: thesis: ( h1 is total & h2 is total implies ( (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) )

then h1 + h2 is total by VFUNCT_1:32;

then dom (h1 + h2) = the carrier of S by PARTFUN1:def 2;

then (dom h1) /\ (dom h2) = the carrier of S by VFUNCT_1:def 1;

then A1: rng seq c= (dom h1) /\ (dom h2) ;

hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NFCONT_1:12; :: thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)

thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, NFCONT_1:12; :: thesis: verum

for seq being sequence of S st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

let h1, h2 be PartFunc of S,T; :: thesis: for seq being sequence of S st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

let seq be sequence of S; :: thesis: ( h1 is total & h2 is total implies ( (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) )

then h1 + h2 is total by VFUNCT_1:32;

then dom (h1 + h2) = the carrier of S by PARTFUN1:def 2;

then (dom h1) /\ (dom h2) = the carrier of S by VFUNCT_1:def 1;

then A1: rng seq c= (dom h1) /\ (dom h2) ;

hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NFCONT_1:12; :: thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)

thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, NFCONT_1:12; :: thesis: verum