let x be Real; :: thesis: ( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
thus (exp_R . 1) #R x = (exp_R 1) #R x by SIN_COS:def 23
.= exp_R x by Th9
.= exp_R . x by SIN_COS:def 23 ; :: thesis: ( (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
thus (exp_R . 1) to_power x = (exp_R 1) to_power x by SIN_COS:def 23
.= exp_R x by Th9
.= exp_R . x by SIN_COS:def 23 ; :: thesis: ( number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
thus number_e to_power x = exp_R x by Th9
.= exp_R . x by SIN_COS:def 23 ; :: thesis: number_e #R x = exp_R . x
thus number_e #R x = exp_R x by Th9
.= exp_R . x by SIN_COS:def 23 ; :: thesis: verum