theorem Th21: :: NDIFF13:20

for E, F, G being RealNormSpace
for u being PartFunc of E,F
for Z being Subset of E
for L being Lipschitzian LinearOperator of F,G st u is_differentiable_on Z holds
( L * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x) ) )