set o = odd_part p;

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

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

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

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

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

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

end;

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

then (odd_part p) . i = p . i by Def2;
hence (odd_part p) . i is Real ; :: thesis: verum

end;

end;

end;

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

end;

hence odd_part p is real ; :: thesis: verum