consider f being PartFunc of D, the carrier of Y such that
A2: X = dom f and
A3: for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) by A1, Th18;
take f ; :: thesis: ( dom f = X & ( for x being Element of D st x in dom f holds
f . x = lim (H # x) ) )
thus dom f = X by A2; :: thesis: for x being Element of D st x in dom f holds
f . x = lim (H # x)
let x be Element of D; :: thesis: ( x in dom f implies f . x = lim (H # x) )
assume x in dom f ; :: thesis: f . x = lim (H # x)
hence f . x = lim (H # x) by A2, A3; :: thesis: verum