let S, T be RealNormSpace; for h1, h2 being PartFunc of S,T
for seq being sequence of S 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 S,T; for seq being sequence of S 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 sequence of S; ( 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
by XBOOLE_1:17;
A2:
(dom h1) /\ (dom h2) c= dom h2
by XBOOLE_1:17;
assume A3:
rng seq c= (dom h1) /\ (dom h2)
; ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
then A4:
rng seq c= dom (h1 + h2)
by VFUNCT_1:def 1;
now for n being Nat holds ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)let n be
Nat;
((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)A5:
n in NAT
by ORDINAL1:def 12;
A6:
seq . n in dom (h1 + h2)
by A4, Th5;
thus ((h1 + h2) /* seq) . n =
(h1 + h2) /. (seq . n)
by A4, FUNCT_2:109, A5
.=
(h1 /. (seq . n)) + (h2 /. (seq . n))
by A6, VFUNCT_1:def 1
.=
((h1 /* seq) . n) + (h2 /. (seq . n))
by A3, A1, FUNCT_2:109, XBOOLE_1:1, A5
.=
((h1 /* seq) . n) + ((h2 /* seq) . n)
by A3, A2, FUNCT_2:109, XBOOLE_1:1, A5
;
verum end;
hence
(h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq)
by NORMSP_1:def 2; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)
A7:
rng seq c= dom (h1 - h2)
by A3, VFUNCT_1:def 2;
now for n being Nat holds ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)let n be
Nat;
((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)A8:
n in NAT
by ORDINAL1:def 12;
A9:
seq . n in dom (h1 - h2)
by A7, Th5;
thus ((h1 - h2) /* seq) . n =
(h1 - h2) /. (seq . n)
by A7, FUNCT_2:109, A8
.=
(h1 /. (seq . n)) - (h2 /. (seq . n))
by A9, VFUNCT_1:def 2
.=
((h1 /* seq) . n) - (h2 /. (seq . n))
by A3, A1, FUNCT_2:109, XBOOLE_1:1, A8
.=
((h1 /* seq) . n) - ((h2 /* seq) . n)
by A3, A2, FUNCT_2:109, XBOOLE_1:1, A8
;
verum end;
hence
(h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)
by NORMSP_1:def 3; verum