let V, V' be RealLinearSpace; :: thesis: ( V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) implies for f being linear-Functional of V' holds f is linear-Functional of V )
assume A1: V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) ; :: thesis: for f being linear-Functional of V' holds f is linear-Functional of V
let f be linear-Functional of V'; :: thesis: f is linear-Functional of V
reconsider f' = f as Functional of V by A1;
A2: f' is additive

proof

let x, y be VECTOR of V; :: according to HAHNBAN:def 4 :: thesis: f' . (x + y) = (f' . x) + (f' . y)
reconsider x' = x, y' = y as VECTOR of V' by A1;
thus f' . (x + y) = f . (x' + y') by A1
.= (f' . x) + (f' . y) by Def4 ; :: thesis: verum

end;

f' is homogeneous

proof

let x be VECTOR of V; :: according to HAHNBAN:def 5 :: thesis: for r being Real holds f' . (r * x) = r * (f' . x)
let r be Real; :: thesis: f' . (r * x) = r * (f' . x)
reconsider x' = x as VECTOR of V' by A1;
thus f' . (r * x) = f' . (r * x') by A1
.= r * (f' . x) by Def5 ; :: thesis: verum

end;

hence f is linear-Functional of V by A2; :: thesis: verum