let seq be Complex_Sequence; :: thesis: for h being PartFunc of COMPLEX,COMPLEX
for Ns being V42() sequence of NAT st rng seq c= dom h holds
Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
let h be PartFunc of COMPLEX,COMPLEX; :: thesis: for Ns being V42() sequence of NAT st rng seq c= dom h holds
Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
let Ns be V42() sequence of NAT; :: thesis: ( rng seq c= dom h implies Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) )
assume A1: rng seq c= dom h ; :: thesis: Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
now :: thesis: for n being Element of NAT holds (Re ((h /* seq) * Ns)) . n = (Re (h /* (seq * Ns))) . n
let n be Element of NAT ; :: thesis: (Re ((h /* seq) * Ns)) . n = (Re (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 (Re ((h /* seq) * Ns)) . n = Re (((h /* seq) * Ns) . n) by COMSEQ_3:def 5
.= Re ((h /* seq) . (Ns . n)) by FUNCT_2:15
.= Re (h /. (seq . (Ns . n))) by A1, FUNCT_2:109
.= Re (h /. ((seq * Ns) . n)) by FUNCT_2:15
.= Re ((h /* (seq * Ns)) . n) by A1, A2, FUNCT_2:109, XBOOLE_1:1
.= (Re (h /* (seq * Ns))) . n by COMSEQ_3:def 5 ; :: thesis: verum
end;
hence Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) by FUNCT_2:63; :: thesis: verum