let g be 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 2;
then rng seq c= dom h ;
hence (g (#) h) /* seq = g (#) (h /* seq) by Th8; :: thesis: verum