let r, p be Real; :: thesis: for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^))
let n be Element of NAT ; :: thesis: (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^))
A1: dom ((r * p) (#) ((#Z n) ^)) = dom ((#Z n) ^) by VALUED_1:def 5
.= dom (p (#) ((#Z n) ^)) by VALUED_1:def 5
.= dom (r (#) (p (#) ((#Z n) ^))) by VALUED_1:def 5 ;

now :: thesis: for c being object st c in dom ((r * p) (#) ((#Z n) ^)) holds
((r * p) (#) ((#Z n) ^)) . c = (r (#) (p (#) ((#Z n) ^))) . c

let c be object ; :: thesis: ( c in dom ((r * p) (#) ((#Z n) ^)) implies ((r * p) (#) ((#Z n) ^)) . c = (r (#) (p (#) ((#Z n) ^))) . c )
assume A2: c in dom ((r * p) (#) ((#Z n) ^)) ; :: thesis: ((r * p) (#) ((#Z n) ^)) . c = (r (#) (p (#) ((#Z n) ^))) . c
then A3: c in dom (p (#) ((#Z n) ^)) by A1, VALUED_1:def 5;
thus ((r * p) (#) ((#Z n) ^)) . c = (r * p) * (((#Z n) ^) . c) by A2, VALUED_1:def 5
.= r * (p * (((#Z n) ^) . c))
.= r * ((p (#) ((#Z n) ^)) . c) by A3, VALUED_1:def 5
.= (r (#) (p (#) ((#Z n) ^))) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum

end;

hence (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^)) by A1, FUNCT_1:2; :: thesis: verum