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