let n be Element of NAT ; :: thesis: for a, b being non empty real number holds (a * b) to_power n = (a to_power n) * (b to_power n)
let a, b be non empty real number ; :: thesis: (a * b) to_power n = (a to_power n) * (b to_power n)
( (a * b) #Z n = (a * b) to_power n & a #Z n = a to_power n & b #Z n = b to_power n ) by POWER:50;
hence (a * b) to_power n = (a to_power n) * (b to_power n) by PREPOWER:50; :: thesis: verum