let X, Y be RealNormSpace; :: thesis: 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) )
let L be Lipschitzian LinearOperator of X,Y; :: thesis: for seq being sequence of X st seq is convergent holds
( L * seq is convergent & lim (L * seq) = L . (lim seq) )
let seq be sequence of X; :: thesis: ( seq is convergent implies ( L * seq is convergent & lim (L * seq) = L . (lim seq) ) )
assume A1: seq is convergent ; :: thesis: ( L * seq is convergent & lim (L * seq) = L . (lim seq) )
A2: L is_continuous_on the carrier of X by LOPBAN_7:6;
A3: the carrier of X = dom L by FUNCT_2:def 1;
A4: rng seq c= the carrier of X ;
lim seq in the carrier of X ;
then A5: ( L /* seq is convergent & L /. (lim seq) = lim (L /* seq) ) by A1, A2, A4, NFCONT_1:18;
rng seq c= dom L by A3;
hence ( L * seq is convergent & lim (L * seq) = L . (lim seq) ) by A5, FUNCT_2:def 11; :: thesis: verum