let n, m be Nat; :: thesis: 0 to_power (n + m) = (0 to_power n) * (0 to_power m)

per cases ( n > 0 or m > 0 or ( n = 0 & m = 0 ) ) ;

suppose A1: ( n > 0 or m > 0 ) ; :: thesis: 0 to_power (n + m) = (0 to_power n) * (0 to_power m)

( 0 to_power (n + m) = 0 & ( 0 to_power n = 0 or 0 to_power m = 0 ) ) by A1, POWER:def 2;
hence 0 to_power (n + m) = (0 to_power n) * (0 to_power m) ; :: thesis: verum

end;

suppose ( n = 0 & m = 0 ) ; :: thesis: 0 to_power (n + m) = (0 to_power n) * (0 to_power m)

then ( 0 to_power (n + m) = 1 & 0 to_power n = 1 & 0 to_power m = 1 ) by POWER:29;
hence 0 to_power (n + m) = (0 to_power n) * (0 to_power m) ; :: thesis: verum

end;

end;