let r be Real; :: thesis: for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let W be non empty set ; :: thesis: for h being PartFunc of W,REAL
for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let seq be sequence of W; :: thesis: ( h is total implies (r (#) h) /* seq = r (#) (h /* seq) )
assume h is total ; :: thesis: (r (#) h) /* seq = r (#) (h /* seq)
then dom h = W by PARTFUN1:def 2;
then rng seq c= dom h ;
hence (r (#) h) /* seq = r (#) (h /* seq) by Th9; :: thesis: verum