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 Def20, Def22;
hence ( cos . th = Sum (th P_cos ) & sin . th = Sum (th P_sin ) ) by Th39; :: thesis: verum