let g be Complex; :: thesis: for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
(g (#) h) /* seq = g (#) (h /* seq)
let seq be Complex_Sequence; :: thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
(g (#) h) /* seq = g (#) (h /* seq)
let h be PartFunc of COMPLEX,COMPLEX; :: thesis: ( rng seq c= dom h implies (g (#) h) /* seq = g (#) (h /* seq) )
assume A1: rng seq c= dom h ; :: thesis: (g (#) h) /* seq = g (#) (h /* seq)
then A2: rng seq c= dom (g (#) h) by VALUED_1:def 5;
now :: thesis: for n being Element of NAT holds ((g (#) h) /* seq) . n = (g (#) (h /* seq)) . n
let n be Element of NAT ; :: thesis: ((g (#) h) /* seq) . n = (g (#) (h /* seq)) . n
A3: seq . n in rng seq by VALUED_0:28;
thus ((g (#) h) /* seq) . n = (g (#) h) /. (seq . n) by A2, FUNCT_2:109
.= g * (h /. (seq . n)) by A2, A3, CFUNCT_1:4
.= g * ((h /* seq) . n) by A1, FUNCT_2:109
.= (g (#) (h /* seq)) . n by VALUED_1:6 ; :: thesis: verum
end;
hence (g (#) h) /* seq = g (#) (h /* seq) by FUNCT_2:63; :: thesis: verum