theorem :: NDIFF11:6

for m, n being non zero Element of NAT
for M being Matrix of m,n,F_Real holds Mx2Tran M is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n)