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;