let r be Real; :: thesis: for f being differentiable Function of REAL,REAL holds (r (#) f) `| = r (#) (f `|)
let f be differentiable Function of REAL,REAL; :: thesis: (r (#) f) `| = r (#) (f `|)
let s be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: ((r (#) f) `|) . s = (r (#) (f `|)) . s
A1: f is_differentiable_in s by Th9;
A2: (f `|) . s = diff (f,s) by Th10;
thus ((r (#) f) `|) . s = diff ((r (#) f),s) by Th10
.= r * (diff (f,s)) by A1, FDIFF_1:15
.= (r (#) (f `|)) . s by A2, VALUED_1:6 ; :: thesis: verum