let X be set ; :: thesis: for seq being Real_Sequence
for h being PartFunc of REAL ,REAL st rng seq c= dom (h | X) & h " {0 } = {} holds
((h ^ ) | X) /* seq = ((h | X) /* seq) "
let seq be Real_Sequence; :: thesis: for h being PartFunc of REAL ,REAL st rng seq c= dom (h | X) & h " {0 } = {} holds
((h ^ ) | X) /* seq = ((h | X) /* seq) "
let h be PartFunc of REAL ,REAL ; :: thesis: ( rng seq c= dom (h | X) & h " {0 } = {} implies ((h ^ ) | X) /* seq = ((h | X) /* seq) " )
assume A1: ( rng seq c= dom (h | X) & h " {0 } = {} ) ; :: thesis: ((h ^ ) | X) /* seq = ((h | X) /* seq) "

now

let x be set ; :: thesis: ( x in rng seq implies x in dom ((h ^ ) | X) )
assume x in rng seq ; :: thesis: x in dom ((h ^ ) | X)
then x in dom (h | X) by A1;
then x in (dom h) /\ X by RELAT_1:90;
then ( x in (dom h) \ (h " {0 }) & x in X ) by A1, XBOOLE_0:def 4;
then ( x in dom (h ^ ) & x in X ) by RFUNCT_1:def 8;
then x in (dom (h ^ )) /\ X by XBOOLE_0:def 4;
hence x in dom ((h ^ ) | X) by RELAT_1:90; :: thesis: verum

end;

then A2: rng seq c= dom ((h ^ ) | X) by TARSKI:def 3;

now

let n be Element of NAT ; :: thesis: (((h ^ ) | X) /* seq) . n = (((h | X) /* seq) " ) . n
A3: seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h | X) by A1;
then seq . n in (dom h) /\ X by RELAT_1:90;
then A4: ( seq . n in (dom h) \ (h " {0 }) & seq . n in X ) by A1, XBOOLE_0:def 4;
then A5: ( seq . n in dom (h ^ ) & seq . n in X ) by RFUNCT_1:def 8;
thus (((h ^ ) | X) /* seq) . n = ((h ^ ) | X) . (seq . n) by A2, FUNCT_2:185
.= (h ^ ) . (seq . n) by A4, FUNCT_1:72
.= (h . (seq . n)) " by A5, RFUNCT_1:def 8
.= ((h | X) . (seq . n)) " by A1, A3, FUNCT_1:70
.= (((h | X) /* seq) . n) " by A1, FUNCT_2:185
.= (((h | X) /* seq) " ) . n by VALUED_1:10 ; :: thesis: verum

end;

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