let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X being set st H is_point_conv_on X holds
for x being Element of D st x in X holds
{x} common_on_dom H
let H be Functional_Sequence of D,REAL; :: thesis: for X being set st H is_point_conv_on X holds
for x being Element of D st x in X holds
{x} common_on_dom H
let X be set ; :: thesis: ( H is_point_conv_on X implies for x being Element of D st x in X holds
{x} common_on_dom H )
assume H is_point_conv_on X ; :: thesis: for x being Element of D st x in X holds
{x} common_on_dom H
then X common_on_dom H by Def12;
hence for x being Element of D st x in X holds
{x} common_on_dom H by Th27; :: thesis: verum