let W be non empty set ; :: thesis: for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h ^) holds

(h ^) /* seq = (h /* seq) "

let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom (h ^) holds

(h ^) /* seq = (h /* seq) "

let seq be sequence of W; :: 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 2, XBOOLE_1:36;

for seq being sequence of W st rng seq c= dom (h ^) holds

(h ^) /* seq = (h /* seq) "

let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom (h ^) holds

(h ^) /* seq = (h /* seq) "

let seq be sequence of W; :: 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 2, XBOOLE_1:36;

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

hence
(h ^) /* seq = (h /* seq) "
by FUNCT_2:63; :: thesis: verumlet 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:108

.= (h . (seq . n)) " by A1, A3, RFUNCT_1:def 2

.= ((h /* seq) . n) " by A2, FUNCT_2:108, XBOOLE_1:1

.= ((h /* seq) ") . n by VALUED_1:10 ; :: thesis: verum

end;A3: seq . n in rng seq by VALUED_0:28;

thus ((h ^) /* seq) . n = (h ^) . (seq . n) by A1, FUNCT_2:108

.= (h . (seq . n)) " by A1, A3, RFUNCT_1:def 2

.= ((h /* seq) . n) " by A2, FUNCT_2:108, XBOOLE_1:1

.= ((h /* seq) ") . n by VALUED_1:10 ; :: thesis: verum