let n, m be Nat; :: thesis: for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is homogeneous iff g is homogeneous )
let f be Function of (REAL m),(REAL n); :: thesis: for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is homogeneous iff g is homogeneous )
let g be Function of (REAL-NS m),(REAL-NS n); :: thesis: ( f = g implies ( f is homogeneous iff g is homogeneous ) )
assume A1: f = g ; :: thesis: ( f is homogeneous iff g is homogeneous )
hereby :: thesis: ( g is homogeneous implies f is homogeneous )
assume A2: f is homogeneous ; :: thesis: g is homogeneous
now :: thesis: for x being Point of (REAL-NS m)
for r being Real holds g . (r * x) = r * (g . x)
let x be Point of (REAL-NS m); :: thesis: for r being Real holds g . (r * x) = r * (g . x)
let r be Real; :: thesis: g . (r * x) = r * (g . x)
reconsider x1 = x as Element of REAL m by REAL_NS1:def 4;
g . (r * x) = f . (r * x1) by A1, REAL_NS1:3
.= r * (f . x1) by A2 ;
hence g . (r * x) = r * (g . x) by A1, REAL_NS1:3; :: thesis: verum
end;
hence g is homogeneous ; :: thesis: verum
end;
assume A3: g is homogeneous ; :: thesis: f is homogeneous
now :: thesis: for x being Element of REAL m
for r being Real holds f . (r * x) = r * (f . x)
let x be Element of REAL m; :: thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; :: thesis: f . (r * x) = r * (f . x)
reconsider x1 = x as Point of (REAL-NS m) by REAL_NS1:def 4;
f . (r * x) = g . (r * x1) by A1, REAL_NS1:3
.= r * (g . x1) by A3 ;
hence f . (r * x) = r * (f . x) by A1, REAL_NS1:3; :: thesis: verum
end;
hence f is homogeneous ; :: thesis: verum