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

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