let n be non zero Nat; :: thesis: for X being RealNormSpace
for f being LinearOperator of (REAL-NS n),X holds f is Lipschitzian
let X be RealNormSpace; :: thesis: for f being LinearOperator of (REAL-NS n),X holds f is Lipschitzian
let f be LinearOperator of (REAL-NS n),X; :: thesis: f is Lipschitzian
( REAL-NS n is finite-dimensional & dim (REAL-NS n) = n ) by REAL_NS2:62;
hence f is Lipschitzian by LOPBAN15:2; :: thesis: verum