theorem :: LOPBAN11:14

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being MultilinearOperator of X,Y holds
( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )