let n be Element of NAT ; :: thesis: for a, b being non zero Real holds (a * b) to_power n = (a to_power n) * (b to_power n)
let a, b be non zero Real; :: thesis: (a * b) to_power n = (a to_power n) * (b to_power n)
A1: b #Z n = b to_power n by POWER:43;
( (a * b) #Z n = (a * b) to_power n & a #Z n = a to_power n ) by POWER:43;
hence (a * b) to_power n = (a to_power n) * (b to_power n) by A1, PREPOWER:40; :: thesis: verum