let th be real number ; :: thesis: ( cos . th = Sum (th P_cos) & sin . th = Sum (th P_sin) )
reconsider th = th as Real by XREAL_0:def 1;
( sin . th = Im (Sum ((th * <i>) ExpSeq)) & cos . th = Re (Sum ((th * <i>) ExpSeq)) ) by Def16, Def18;
hence ( cos . th = Sum (th P_cos) & sin . th = Sum (th P_sin) ) by Th36; :: thesis: verum