set e = even_part p;

now :: thesis: for i being Nat holds (even_part p) . i is Real

let i be Nat; :: thesis: (even_part p) . i is Real

now :: thesis: ( ( i is odd & (even_part p) . i is Real ) or ( i is even & (even_part p) . i is Real ) )

per cases ( i is odd or i is even ) ;

case i is odd ; :: thesis: (even_part p) . i is Real

then (even_part p) . i = 0. F_Complex by Def1
.= 0 by COMPLFLD:def 1 ;
hence (even_part p) . i is Real ; :: thesis: verum

end;

case i is even ; :: thesis: (even_part p) . i is Real

then (even_part p) . i = p . i by Def1;
hence (even_part p) . i is Real ; :: thesis: verum

end;

end;

end;

hence (even_part p) . i is Real ; :: thesis: verum

end;

hence even_part p is real ; :: thesis: verum