let D be non empty set ; :: thesis:
let H be Functional_Sequence of D,REAL; :: thesis:
let X be set ; :: thesis:
defpred S₁[ set ] means $1 in X;
deffunc H₁( Element of D) -> Element of REAL = In ((lim (H # $1)),REAL);
consider f being PartFunc of D,REAL such that
A1: for x being Element of D holds
( x in dom f iff S₁[x] ) and
A2: for x being Element of D st x in dom f holds
f . x = H₁(x) from SEQ_1:sch 3();
thus ( H is_point_conv_on X implies ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) ) ) :: thesis:

assume A3: H is_point_conv_on X ; :: thesis:
hence X common_on_dom H ; :: thesis:
let x be Element of D; :: thesis:
assume A4: x in X ; :: thesis:
ex f being PartFunc of D,REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) by A3, Th18;
hence H # x is convergent by A4; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in X ; :: thesis:
X c= dom (H . 0) by A5;
then X c= D by XBOOLE_1:1;
then reconsider x9 = x as Element of D by A8;
x9 in dom f by A1, A8;
hence x in dom f ; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dom f ; :: thesis:
hence x in X by A1; :: thesis:

end;

let x be Element of D; :: thesis:
assume A9: x in X ; :: thesis:
hence H # x is convergent by A6; :: thesis:
thus f . x = H₁(x) by A2, A7, A9
.= lim (H # x) ; :: thesis:

end;