let n be natural number ; :: thesis: for r being non empty real number st n is even holds
r to_power n > 0
let r be non empty real number ; :: 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;