let g be Element of COMPLEX ; :: thesis: for seq being Complex_Sequence
for h being PartFunc of COMPLEX ,COMPLEX st h is total holds
(g (#) h) /* seq = g (#) (h /* seq)
let seq be Complex_Sequence; :: thesis: for h being PartFunc of COMPLEX ,COMPLEX st h is total holds
(g (#) h) /* seq = g (#) (h /* seq)
let h be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( h is total implies (g (#) h) /* seq = g (#) (h /* seq) )
assume h is total ; :: thesis: (g (#) h) /* seq = g (#) (h /* seq)
then dom h = COMPLEX by PARTFUN1:def 4;
then rng seq c= dom h ;
hence (g (#) h) /* seq = g (#) (h /* seq) by Th19; :: thesis: verum