let seq be Real_Sequence; :: thesis: for h being PartFunc of REAL ,REAL st rng seq c= dom (h ^ ) holds
(h ^ ) /* seq = (h /* seq) "
let h be PartFunc of REAL ,REAL ; :: thesis: ( rng seq c= dom (h ^ ) implies (h ^ ) /* seq = (h /* seq) " )
assume A1: rng seq c= dom (h ^ ) ; :: thesis: (h ^ ) /* seq = (h /* seq) "
then A2: ( (dom h) \ (h " {0 }) c= dom h & rng seq c= (dom h) \ (h " {0 }) ) by RFUNCT_1:def 8, XBOOLE_1:36;

now

let n be Element of NAT ; :: thesis: ((h ^ ) /* seq) . n = ((h /* seq) " ) . n
A3: seq . n in rng seq by VALUED_0:28;
thus ((h ^ ) /* seq) . n = (h ^ ) . (seq . n) by A1, FUNCT_2:185
.= (h . (seq . n)) " by A1, A3, RFUNCT_1:def 8
.= ((h /* seq) . n) " by A2, FUNCT_2:185, XBOOLE_1:1
.= ((h /* seq) " ) . n by VALUED_1:10 ; :: thesis: verum

end;

hence (h ^ ) /* seq = (h /* seq) " by FUNCT_2:113; :: thesis: verum