for X being RealBanachSpace
for Y being RealNormSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )