let r be Element of REAL ; :: thesis: for seq being Real_Sequence
for h being PartFunc of REAL,REAL st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let seq be Real_Sequence; :: thesis: for h being PartFunc of REAL,REAL st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
let h be PartFunc of REAL,REAL; :: 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 = REAL by PARTFUN1:def 2;
then rng seq c= dom h ;
hence (r (#) h) /* seq = r (#) (h /* seq) by Th24; :: thesis: verum