let V be non empty VectSp of F_Complex ; :: thesis: for l being linear-Functional of V holds projIm l is linear-Functional of (RealVS V)
let l be linear-Functional of V; :: thesis: projIm l is linear-Functional of (RealVS V)
A1: projIm l is additive

proof

let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def 4 :: thesis: (projIm l) . (x + y) = ((projIm l) . x) + ((projIm l) . y)
A2: addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
then reconsider x1 = x, y1 = y as Vector of V ;
thus (projIm l) . (x + y) = Im (l . (x1 + y1)) by A2, Def24
.= Im ((l . x1) + (l . y1)) by Def11
.= (Im (l . x1)) + (Im (l . y1)) by COMPLEX1:19
.= (Im (l . x1)) + ((projIm l) . y) by Def24
.= ((projIm l) . x) + ((projIm l) . y) by Def24 ; :: thesis: verum

end;

projIm l is homogeneous

proof

let x be VECTOR of (RealVS V); :: according to HAHNBAN:def 5 :: thesis: for b₁ being Element of REAL holds (projIm l) . (b₁ * x) = b₁ * ((projIm l) . x)
let r be Real; :: thesis: (projIm l) . (r * x) = r * ((projIm l) . x)
addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0 **] * x1 by Def22;
hence (projIm l) . (r * x) = Im (l . ([**r,0 **] * x1)) by Def24
.= Im ([**r,0 **] * (l . x1)) by Def12
.= ((Re [**r,0 **]) * (Im (l . x1))) + ((Re (l . x1)) * (Im [**r,0 **])) by COMPLEX1:24
.= ((Re [**r,0 **]) * (Im (l . x1))) + ((Re (l . x1)) * 0 ) by COMPLEX1:28
.= r * (Im (l . x1)) by COMPLEX1:28
.= r * ((projIm l) . x) by Def24 ;
:: thesis: verum

end;

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