let S be RealNormSpace; :: thesis: for h1, h2 being PartFunc of REAL, the carrier of S
for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let h1, h2 be PartFunc of REAL, the carrier of S; :: thesis: for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let seq be Real_Sequence; :: thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) )
A1: ( (dom h1) /\ (dom h2) c= dom h1 & (dom h1) /\ (dom h2) c= dom h2 ) by XBOOLE_1:17;
assume A2: rng seq c= (dom h1) /\ (dom h2) ; :: thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

now :: thesis: for n being Nat holds ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)

let n be Nat; :: thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)
A3: n in NAT by ORDINAL1:def 12;
A4: ( h1 /. (seq . n) = (h1 /* seq) . n & h2 /. (seq . n) = (h2 /* seq) . n ) by A1, A2, FUNCT_2:109, XBOOLE_1:1, A3;
A5: rng seq c= dom (h1 + h2) by A2, VFUNCT_1:def 1;
then A6: seq . n in dom (h1 + h2) by Th1;
thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A5, FUNCT_2:109, A3
.= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A4, A6, VFUNCT_1:def 1 ; :: thesis: verum

end;

hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NORMSP_1:def 2; :: thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)

now :: thesis: for n being Nat holds ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)

let n be Nat; :: thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)
A7: n in NAT by ORDINAL1:def 12;
A8: ( h1 /. (seq . n) = (h1 /* seq) . n & h2 /. (seq . n) = (h2 /* seq) . n ) by A1, A2, FUNCT_2:109, XBOOLE_1:1, A7;
A9: rng seq c= dom (h1 - h2) by A2, VFUNCT_1:def 2;
then A10: seq . n in dom (h1 - h2) by Th1;
thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A9, FUNCT_2:109, A7
.= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A8, A10, VFUNCT_1:def 2 ; :: thesis: verum

end;

hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by NORMSP_1:def 3; :: thesis: verum