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)

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

end;

suppose A2: ( 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 by POWER:24;
hence 0 to_power (n + m) = (0 to_power n) * (0 to_power m) by A2; :: thesis: verum

end;

end;