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 set st H is_point_conv_on X holds
( ||.H.|| is_point_conv_on X & lim (||.H.||,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_point_conv_on X holds
( ||.H.|| is_point_conv_on X & lim (||.H.||,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st H is_point_conv_on X holds
( ||.H.|| is_point_conv_on X & lim (||.H.||,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
let X be set ; :: thesis: ( H is_point_conv_on X implies ( ||.H.|| is_point_conv_on X & lim (||.H.||,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) )
assume A1: H is_point_conv_on X ; :: thesis: ( ||.H.|| is_point_conv_on X & lim (||.H.||,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )

A2: now :: thesis: for x being Element of D st x in X holds
||.H.|| # x is convergent

let x be Element of D; :: thesis: ( x in X implies ||.H.|| # x is convergent )
assume X0: x in X ; :: thesis: ||.H.|| # x is convergent
then X1: {x} common_on_dom H by A1, Th25;
||.(H # x).|| is convergent by X0, A1, Th19, NORMSP_1:23;
hence ||.H.|| # x is convergent by Th28, X1; :: thesis: verum

end;

A3: now :: thesis: for x being Element of D st x in dom (- (lim (H,X))) holds
(- (lim (H,X))) . x = lim ((- H) # x)

let x be Element of D; :: thesis: ( x in dom (- (lim (H,X))) implies (- (lim (H,X))) . x = lim ((- H) # x) )
assume A30: x in dom (- (lim (H,X))) ; :: thesis: (- (lim (H,X))) . x = lim ((- H) # x)
then A4: x in dom (lim (H,X)) by VFUNCT_1:def 5;
then A5: x in X by A1, Def13;
X5: (lim (H,X)) /. x = (lim (H,X)) . x by A4, PARTFUN1:def 6;
X1: {x} common_on_dom H by A5, A1, Th25;
thus (- (lim (H,X))) . x = (- (lim (H,X))) /. x by A30, PARTFUN1:def 6
.= - ((lim (H,X)) /. x) by A30, VFUNCT_1:def 5
.= - (lim (H # x)) by X5, A1, A4, Def13
.= (- 1) * (lim (H # x)) by RLVECT_1:16
.= lim ((- 1) * (H # x)) by A1, A5, Th19, NORMSP_1:28
.= lim ((- H) # x) by Th28, X1 ; :: thesis: verum

end;

thus A7: ||.H.|| is_point_conv_on X by A1, Th37, A2, SEQFUNC:20; :: thesis: ( lim (||.H.||,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )

A8: now :: thesis: for x being Element of D st x in dom ||.(lim (H,X)).|| holds
||.(lim (H,X)).|| . x = lim (||.H.|| # x)

let x be Element of D; :: thesis: ( x in dom ||.(lim (H,X)).|| implies ||.(lim (H,X)).|| . x = lim (||.H.|| # x) )
assume A91: x in dom ||.(lim (H,X)).|| ; :: thesis: ||.(lim (H,X)).|| . x = lim (||.H.|| # x)
then A9: x in dom (lim (H,X)) by NORMSP_0:def 3;
then A90: x in X by A1, Def13;
then A10: H # x is convergent by A1, Th19;
X1: {x} common_on_dom H by A90, A1, Th25;
X10: (lim (H,X)) /. x = (lim (H,X)) . x by A9, PARTFUN1:def 6;
thus ||.(lim (H,X)).|| . x = ||.((lim (H,X)) /. x).|| by A91, NORMSP_0:def 3
.= ||.(lim (H # x)).|| by A1, A9, X10, Def13
.= lim ||.(H # x).|| by A10, LOPBAN_1:20
.= lim (||.H.|| # x) by Th28, X1 ; :: thesis: verum

end;

A11: now :: thesis: for x being Element of D st x in X holds
(- H) # x is convergent

let x be Element of D; :: thesis: ( x in X implies (- H) # x is convergent )
assume A90: x in X ; :: thesis: (- H) # x is convergent
then X10: (- 1) * (H # x) is convergent by A1, Th19, NORMSP_1:22;
{x} common_on_dom H by A90, A1, Th25;
hence (- H) # x is convergent by Th28, X10; :: thesis: verum

end;

dom ||.(lim (H,X)).|| = dom (lim (H,X)) by NORMSP_0:def 3
.= X by A1, Def13 ;
hence lim (||.H.||,X) = ||.(lim (H,X)).|| by A7, A8, SEQFUNC:def 13; :: thesis: ( - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
thus A12: - H is_point_conv_on X by A1, Th37, A11, Th19; :: thesis: lim ((- H),X) = - (lim (H,X))
dom (- (lim (H,X))) = dom (lim (H,X)) by VFUNCT_1:def 5
.= X by A1, Def13 ;
hence lim ((- H),X) = - (lim (H,X)) by A12, A3, Def13; :: thesis: verum