let m, n be non zero Element of NAT ; :: thesis: for M being Matrix of m,n,F_Real holds Mx2Tran M is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n)
let M be Matrix of m,n,F_Real; :: thesis: Mx2Tran M is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n)
( the carrier of (TOP-REAL n) = the carrier of (REAL-NS n) & the carrier of (TOP-REAL m) = the carrier of (REAL-NS m) ) by REAL_NS2:4;
then reconsider f = Mx2Tran M as Function of (REAL-NS m),(REAL-NS n) ;
for x, y being Element of (REAL-NS m) holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Element of (REAL-NS m); :: thesis: f . (x + y) = (f . x) + (f . y)
reconsider x0 = x, y0 = y as Element of (TOP-REAL m) by REAL_NS2:4;
thus f . (x + y) = (Mx2Tran M) . (x0 + y0) by REAL_NS2:7
.= ((Mx2Tran M) . x0) + ((Mx2Tran M) . y0) by MATRTOP1:22
.= (f . x) + (f . y) by REAL_NS2:7 ; :: thesis: verum

end;

then A1: f is additive ;
for x being VECTOR of (REAL-NS m)
for a being Real holds f . (a * x) = a * (f . x)

proof

let x be VECTOR of (REAL-NS m); :: thesis: for a being Real holds f . (a * x) = a * (f . x)
let a be Real; :: thesis: f . (a * x) = a * (f . x)
reconsider x0 = x as Element of (TOP-REAL m) by REAL_NS2:4;
thus f . (a * x) = (Mx2Tran M) . (a * x0) by REAL_NS2:8
.= a * ((Mx2Tran M) . x0) by MATRTOP1:23
.= a * (f . x) by REAL_NS2:8 ; :: thesis: verum

end;

then reconsider f = f as LinearOperator of (REAL-NS m),(REAL-NS n) by A1, LOPBAN_1:def 5;
( REAL-NS m is finite-dimensional & dim (REAL-NS m) = m ) by REAL_NS2:62;
then f is Lipschitzian by LOPBAN15:2;
hence Mx2Tran M is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) ; :: thesis: verum