let th be Real; :: thesis: exp (th * <i>) = (cos th) + ((sin th) * <i>)
exp (th * <i>) = Sum ((th * <i>) ExpSeq) by Def14
.= (cos th) + ((sin th) * <i>) by Lm3 ;
hence exp (th * <i>) = (cos th) + ((sin th) * <i>) ; :: thesis: verum