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

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