let D be non empty set ; :: thesis:
let Y be RealNormSpace; :: thesis:
let H be Functional_Sequence of D, the carrier of Y; :: thesis:
let X be set ; :: thesis:
assume A1: H is_point_conv_on X ; :: thesis:

A2: now :: thesis:

let x be Element of D; :: thesis:
assume X0: x in X ; :: thesis:
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:

end;

A3: now :: thesis:

let x be Element of D; :: thesis:
assume A30: x in dom (- (lim (H,X))) ; :: thesis:
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:

end;

thus A7: ||.H.|| is_point_conv_on X by A1, Th37, A2, SEQFUNC:20; :: thesis:

A8: now :: thesis:

let x be Element of D; :: thesis:
assume A91: x in dom ||.(lim (H,X)).|| ; :: thesis:
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:

end;

A11: now :: thesis:

let x be Element of D; :: thesis:
assume A90: x in X ; :: thesis:
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:

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:
thus A12: - H is_point_conv_on X by A1, Th37, A11, Th19; :: thesis:
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: