let a be Real; :: thesis: for n being Nat st n is even holds
(- a) |^ n = a |^ n
let n be Nat; :: thesis: ( n is even implies (- a) |^ n = a |^ n )
given m being Nat such that A1: n = 2 * m ; :: according to ABIAN:def 2 :: thesis: (- a) |^ n = a |^ n
thus (- a) |^ n = ((- a) |^ (1 + 1)) |^ m by A1, NEWTON:9
.= (((- a) |^ (0 + 1)) * ((- a) |^ (0 + 1))) |^ m by NEWTON:8
.= ((((- a) |^ 0) * (- a)) * ((- a) |^ (0 + 1))) |^ m by NEWTON:6
.= ((((- a) |^ 0) * (- a)) * (((- a) |^ 0) * (- a))) |^ m by NEWTON:6
.= (((((- a) GeoSeq) . 0) * (- a)) * (((- a) |^ 0) * (- a))) |^ m by PREPOWER:def 1
.= (((((- a) GeoSeq) . 0) * (- a)) * ((((- a) GeoSeq) . 0) * (- a))) |^ m by PREPOWER:def 1
.= (((((- a) GeoSeq) . 0) * (- a)) * (1 * (- a))) |^ m by PREPOWER:3
.= ((1 * (- a)) * (1 * (- a))) |^ m by PREPOWER:3
.= (a * a) |^ m
.= ((((a GeoSeq) . 0) * a) * (1 * a)) |^ m by PREPOWER:3
.= ((((a GeoSeq) . 0) * a) * (((a GeoSeq) . 0) * a)) |^ m by PREPOWER:3
.= ((((a GeoSeq) . 0) * a) * ((a |^ 0) * a)) |^ m by PREPOWER:def 1
.= (((a |^ 0) * a) * ((a |^ 0) * a)) |^ m by PREPOWER:def 1
.= (((a |^ 0) * a) * (a |^ (0 + 1))) |^ m by NEWTON:6
.= ((a |^ (0 + 1)) * (a |^ (0 + 1))) |^ m by NEWTON:6
.= (a |^ (1 + 1)) |^ m by NEWTON:8
.= a |^ n by A1, NEWTON:9 ; :: thesis: verum