let f be LinearOperator of (REAL-NS m),(REAL-NS n); :: thesis: f is Lipschitzian
reconsider g = f as LinearOperator of m,n by Th14;
consider K being Real such that
A1: ( 0 <= K & ( for x being Element of REAL m holds |.(g . x).| <= K * |.x.| ) ) by Def3;
take K ; :: according to LOPBAN_1:def 8 :: thesis: ( 0 <= K & ( for b₁ being Element of the carrier of (REAL-NS m) holds ||.(f . b₁).|| <= K * ||.b₁.|| ) )
thus 0 <= K by A1; :: thesis: for b₁ being Element of the carrier of (REAL-NS m) holds ||.(f . b₁).|| <= K * ||.b₁.||
let x be Point of (REAL-NS m); :: thesis: ||.(f . x).|| <= K * ||.x.||
reconsider x1 = x as Element of REAL m by REAL_NS1:def 4;
reconsider y = g . x1 as Element of REAL n ;
||.(f . x).|| = |.y.| by REAL_NS1:1;
then ||.(f . x).|| <= K * |.x1.| by A1;
hence ||.(f . x).|| <= K * ||.x.|| by REAL_NS1:1; :: thesis: verum