let V be VectSp of F_Complex ; :: thesis: for l being linear-Functional of V holds projRe l is linear-Functional of (RealVS V)
let l be linear-Functional of V; :: thesis: projRe l is linear-Functional of (RealVS V)
A1: projRe l is homogeneous

proof

let x be VECTOR of (RealVS V); :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds (projRe l) . (b₁ * x) = b₁ * ((projRe l) . x)
let r be Real; :: thesis: (projRe l) . (r * x) = r * ((projRe l) . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0**] * x1 by Def17;
hence (projRe l) . (r * x) = Re (l . ([**r,0**] * x1)) by Def18
.= Re ([**r,0**] * (l . x1)) by Def8
.= ((Re [**r,0**]) * (Re (l . x1))) - ((Im [**r,0**]) * (Im (l . x1))) by COMPLEX1:9
.= ((Re [**r,0**]) * (Re (l . x1))) - (0 * (Im (l . x1))) by COMPLEX1:12
.= r * (Re (l . x1)) by COMPLEX1:12
.= r * ((projRe l) . x) by Def18 ;
:: thesis: verum

end;

projRe l is additive

proof

let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def 2 :: thesis: (projRe l) . (x + y) = ((projRe l) . x) + ((projRe l) . y)
A2: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as Vector of V ;
thus (projRe l) . (x + y) = Re (l . (x1 + y1)) by A2, Def18
.= Re ((l . x1) + (l . y1)) by VECTSP_1:def 20
.= (Re (l . x1)) + (Re (l . y1)) by COMPLEX1:8
.= (Re (l . x1)) + ((projRe l) . y) by Def18
.= ((projRe l) . x) + ((projRe l) . y) by Def18 ; :: thesis: verum

end;

hence projRe l is linear-Functional of (RealVS V) by A1; :: thesis: verum