let seq be Complex_Sequence; :: thesis: for h being PartFunc of COMPLEX,COMPLEX
for Ns being increasing sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))
let h be PartFunc of COMPLEX,COMPLEX; :: thesis: for Ns being increasing sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))
let Ns be increasing sequence of NAT; :: thesis: ( rng seq c= dom h implies Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) )
assume A1: rng seq c= dom h ; :: thesis: Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))

now :: thesis: for n being Element of NAT holds (Im ((h /* seq) * Ns)) . n = (Im (h /* (seq * Ns))) . n

let n be Element of NAT ; :: thesis: (Im ((h /* seq) * Ns)) . n = (Im (h /* (seq * Ns))) . n
seq * Ns is subsequence of seq by VALUED_0:def 17;
then A2: rng (seq * Ns) c= rng seq by VALUED_0:21;
thus (Im ((h /* seq) * Ns)) . n = Im (((h /* seq) * Ns) . n) by COMSEQ_3:def 6
.= Im ((h /* seq) . (Ns . n)) by FUNCT_2:15
.= Im (h /. (seq . (Ns . n))) by A1, FUNCT_2:109
.= Im (h /. ((seq * Ns) . n)) by FUNCT_2:15
.= Im ((h /* (seq * Ns)) . n) by A1, A2, FUNCT_2:109, XBOOLE_1:1
.= (Im (h /* (seq * Ns))) . n by COMSEQ_3:def 6 ; :: thesis: verum

end;

hence Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) by FUNCT_2:63; :: thesis: verum