let D be non empty set ; :: thesis: for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
let Y be RealNormSpace; :: thesis: for H1, H2 being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
let H1, H2 be Functional_Sequence of D, the carrier of Y; :: thesis: for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
let x be Element of D; :: thesis: ( {x} common_on_dom H1 & {x} common_on_dom H2 implies ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x ) )
assume that
A1: {x} common_on_dom H1 and
A2: {x} common_on_dom H2 ; :: thesis: ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )

now :: thesis: for n being Element of NAT holds ((H1 # x) + (H2 # x)) . n = ((H1 + H2) # x) . n

let n be Element of NAT ; :: thesis: ((H1 # x) + (H2 # x)) . n = ((H1 + H2) # x) . n
A3: {x} c= dom (H2 . n) by A2;
( x in {x} & {x} c= dom (H1 . n) ) by A1, TARSKI:def 1;
then x in (dom (H1 . n)) /\ (dom (H2 . n)) by A3, XBOOLE_0:def 4;
then A4: x in dom ((H1 . n) + (H2 . n)) by VFUNCT_1:def 1;
X4: dom ((H1 . n) + (H2 . n)) = dom ((H1 + H2) . n) by Def5;
thus ((H1 # x) + (H2 # x)) . n = ((H1 # x) . n) + ((H2 # x) . n) by NORMSP_1:def 2
.= ((H1 . n) /. x) + ((H2 # x) . n) by Def10
.= ((H1 . n) /. x) + ((H2 . n) /. x) by Def10
.= ((H1 . n) + (H2 . n)) /. x by A4, VFUNCT_1:def 1
.= ((H1 . n) + (H2 . n)) . x by A4, PARTFUN1:def 6
.= ((H1 + H2) . n) . x by Def5
.= ((H1 + H2) . n) /. x by A4, X4, PARTFUN1:def 6
.= ((H1 + H2) # x) . n by Def10 ; :: thesis: verum

end;

hence (H1 # x) + (H2 # x) = (H1 + H2) # x by FUNCT_2:63; :: thesis: (H1 # x) - (H2 # x) = (H1 - H2) # x

now :: thesis: for n being Element of NAT holds ((H1 # x) - (H2 # x)) . n = ((H1 - H2) # x) . n

let n be Element of NAT ; :: thesis: ((H1 # x) - (H2 # x)) . n = ((H1 - H2) # x) . n
A5: {x} c= dom (H2 . n) by A2;
( x in {x} & {x} c= dom (H1 . n) ) by A1, TARSKI:def 1;
then x in (dom (H1 . n)) /\ (dom (H2 . n)) by A5, XBOOLE_0:def 4;
then A6: x in dom ((H1 . n) - (H2 . n)) by VFUNCT_1:def 2;
X6: dom ((H1 . n) - (H2 . n)) = dom ((H1 - H2) . n) by Th3;
thus ((H1 # x) - (H2 # x)) . n = ((H1 # x) . n) - ((H2 # x) . n) by NORMSP_1:def 3
.= ((H1 . n) /. x) - ((H2 # x) . n) by Def10
.= ((H1 . n) /. x) - ((H2 . n) /. x) by Def10
.= ((H1 . n) - (H2 . n)) /. x by A6, VFUNCT_1:def 2
.= ((H1 . n) - (H2 . n)) . x by A6, PARTFUN1:def 6
.= ((H1 - H2) . n) . x by Th3
.= ((H1 - H2) . n) /. x by X6, A6, PARTFUN1:def 6
.= ((H1 - H2) # x) . n by Def10 ; :: thesis: verum

end;

hence (H1 # x) - (H2 # x) = (H1 - H2) # x by FUNCT_2:63; :: thesis: verum