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

let c be set ; :: 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:9; :: thesis: verum