for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y
for seq being sequence of X st seq is convergent holds
( L * seq is convergent & lim (L * seq) = L . (lim seq) )