set e = even_part p;

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

hence
even_part p is real
; :: thesis: verumlet i be Nat; :: thesis: (even_part p) . i is Real

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

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