let n, m be Nat; :: thesis: for f being set holds
( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )
let f be set ; :: thesis: ( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )
( REAL m = the carrier of (REAL-NS m) & REAL n = the carrier of (REAL-NS n) ) by REAL_NS1:def 4;
hence ( f is additive homogeneous Function of (REAL m),(REAL n) iff f is additive homogeneous Function of (REAL-NS m),(REAL-NS n) ) by Th12, Th13; :: thesis: verum