let r be Real; :: thesis: for X being set

for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )

assume A1: X c= dom f ; :: thesis: ( not f | X is continuous or (r (#) f) | X is continuous )

assume A2: f | X is continuous ; :: thesis: (r (#) f) | X is continuous

A3: X c= dom (r (#) f) by A1, VALUED_1:def 5;

for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )

assume A1: X c= dom f ; :: thesis: ( not f | X is continuous or (r (#) f) | X is continuous )

assume A2: f | X is continuous ; :: thesis: (r (#) f) | X is continuous

A3: X c= dom (r (#) f) by A1, VALUED_1:def 5;

now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )

hence
(r (#) f) | X is continuous
by A3, Th13; :: thesis: verum( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )

let s1 be Real_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) )

assume that

A4: rng s1 c= X and

A5: s1 is convergent and

A6: lim s1 in X ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )

A7: f /* s1 is convergent by A1, A2, A4, A5, A6, Th13;

then A8: r (#) (f /* s1) is convergent ;

f . (lim s1) = lim (f /* s1) by A1, A2, A4, A5, A6, Th13;

then (r (#) f) . (lim s1) = r * (lim (f /* s1)) by A3, A6, VALUED_1:def 5

.= lim (r (#) (f /* s1)) by A7, SEQ_2:8

.= lim ((r (#) f) /* s1) by A1, A4, RFUNCT_2:9, XBOOLE_1:1 ;

hence ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) by A1, A4, A8, RFUNCT_2:9, XBOOLE_1:1; :: thesis: verum

end;assume that

A4: rng s1 c= X and

A5: s1 is convergent and

A6: lim s1 in X ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )

A7: f /* s1 is convergent by A1, A2, A4, A5, A6, Th13;

then A8: r (#) (f /* s1) is convergent ;

f . (lim s1) = lim (f /* s1) by A1, A2, A4, A5, A6, Th13;

then (r (#) f) . (lim s1) = r * (lim (f /* s1)) by A3, A6, VALUED_1:def 5

.= lim (r (#) (f /* s1)) by A7, SEQ_2:8

.= lim ((r (#) f) /* s1) by A1, A4, RFUNCT_2:9, XBOOLE_1:1 ;

hence ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) by A1, A4, A8, RFUNCT_2:9, XBOOLE_1:1; :: thesis: verum