let n be Nat; :: thesis: for r being non zero Real st n is even holds
r to_power n > 0
let r be non zero Real; :: thesis: ( n is even implies r to_power n > 0 )
assume A1: n is even ; :: thesis: r to_power n > 0
per cases ( r > 0 or r < 0 ) ;
suppose r > 0 ; :: thesis: r to_power n > 0
hence r to_power n > 0 by POWER:34; :: thesis: verum
end;
suppose A2: r < 0 ; :: thesis: r to_power n > 0
r to_power n = (- r) to_power n by Th3, A1;
hence r to_power n > 0 by A2, POWER:34; :: thesis: verum
end;
end;