let V, V9 be RealLinearSpace; :: thesis: ( V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) implies for f being linear-Functional of V holds f is linear-Functional of V9 )
assume A1: V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; :: thesis: for f being linear-Functional of V holds f is linear-Functional of V9
let f be linear-Functional of V; :: thesis: f is linear-Functional of V9
reconsider f9 = f as Functional of V9 by A1;
A2: f9 is homogeneous
proof
let x be VECTOR of V9; :: according to HAHNBAN:def 3 :: thesis: for r being Real holds f9 . (r * x) = r * (f9 . x)
let r be Real; :: thesis: f9 . (r * x) = r * (f9 . x)
reconsider x9 = x as VECTOR of V by A1;
thus f9 . (r * x) = f9 . (r * x9) by A1
.= r * (f9 . x) by Def3 ; :: thesis: verum
end;
f9 is additive
proof
let x, y be VECTOR of V9; :: according to HAHNBAN:def 2 :: thesis: f9 . (x + y) = (f9 . x) + (f9 . y)
reconsider x9 = x, y9 = y as VECTOR of V by A1;
thus f9 . (x + y) = f . (x9 + y9) by A1
.= (f9 . x) + (f9 . y) by Def2 ; :: thesis: verum
end;
hence f is linear-Functional of V9 by A2; :: thesis: verum