set f = the non constant non trivial additive homogeneous Functional of V;
reconsider g = the non constant non trivial additive homogeneous Functional of V as FrFunctional of V by FUNCT_2:7, NUMBERS:15;
take g ; :: thesis: ( g is additive & g is homogeneous & not g is constant & not g is trivial )
for x, y being Vector of V holds g . (x + y) = (g . x) + (g . y)
proof
let x, y be Vector of V; :: thesis: g . (x + y) = (g . x) + (g . y)
thus g . (x + y) = ( the non constant non trivial additive homogeneous Functional of V . x) + ( the non constant non trivial additive homogeneous Functional of V . y) by VECTSP_1:def 20
.= (g . x) + (g . y) ; :: thesis: verum
end;
hence g is additive ; :: thesis: ( g is homogeneous & not g is constant & not g is trivial )
for x being Vector of V
for r being Element of INT.Ring holds g . (r * x) = r * (g . x)
proof
let x be Vector of V; :: thesis: for r being Element of INT.Ring holds g . (r * x) = r * (g . x)
let r be Element of INT.Ring; :: thesis: g . (r * x) = r * (g . x)
thus g . (r * x) = r * ( the non constant non trivial additive homogeneous Functional of V . x) by HAHNBAN1:def 8
.= r * (g . x) ; :: thesis: verum
end;
hence g is homogeneous ; :: thesis: ( not g is constant & not g is trivial )
thus ( not g is constant & not g is trivial ) ; :: thesis: verum