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