let D be non empty set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H holds
( ||.H.|| # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) )
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H holds
( ||.H.|| # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) )
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for x being Element of D st {x} common_on_dom H holds
( ||.H.|| # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) )
let x be Element of D; :: thesis: ( {x} common_on_dom H implies ( ||.H.|| # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) ) )
assume AS1: {x} common_on_dom H ; :: thesis: ( ||.H.|| # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) )

now :: thesis: for n being Element of NAT holds (||.H.|| # x) . n = ||.(H # x).|| . n

let n be Element of NAT ; :: thesis: (||.H.|| # x) . n = ||.(H # x).|| . n
( x in {x} & {x} c= dom (H . n) ) by AS1, TARSKI:def 1;
then x in dom (H . n) ;
then A2: x in dom ||.(H . n).|| by NORMSP_0:def 2;
thus (||.H.|| # x) . n = (||.H.|| . n) . x by SEQFUNC:def 10
.= ||.(H . n).|| . x by Def4
.= ||.((H . n) /. x).|| by A2, NORMSP_0:def 2
.= ||.((H # x) . n).|| by Def10
.= ||.(H # x).|| . n by NORMSP_0:def 4 ; :: thesis: verum

end;

hence ||.H.|| # x = ||.(H # x).|| by FUNCT_2:63; :: thesis: (- H) # x = (- 1) * (H # x)

now :: thesis: for n being Element of NAT holds ((- H) # x) . n = ((- 1) * (H # x)) . n

let n be Element of NAT ; :: thesis: ((- H) # x) . n = ((- 1) * (H # x)) . n
( x in {x} & {x} c= dom (H . n) ) by AS1, TARSKI:def 1;
then x in dom (H . n) ;
then A2: x in dom (- (H . n)) by VFUNCT_1:def 5;
thus ((- H) # x) . n = ((- H) . n) /. x by Def10
.= (- (H . n)) /. x by Def3
.= - ((H . n) /. x) by A2, VFUNCT_1:def 5
.= - ((H # x) . n) by Def10
.= (- 1) * ((H # x) . n) by RLVECT_1:16
.= ((- 1) * (H # x)) . n by NORMSP_1:def 5 ; :: thesis: verum

end;

hence (- H) # x = (- 1) * (H # x) by FUNCT_2:63; :: thesis: verum