let a be real number ; :: thesis: for n being Element of NAT st n is even holds
(- a) |^ n = a |^ n
let n be Element of NAT ; :: thesis: ( n is even implies (- a) |^ n = a |^ n )
given m being Element of 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:14
.= (((- a) |^ (0 + 1)) * ((- a) |^ (0 + 1))) |^ m by NEWTON:13
.= ((((- a) |^ 0 ) * (- a)) * ((- a) |^ (0 + 1))) |^ m by NEWTON:11
.= ((((- a) |^ 0 ) * (- a)) * (((- a) |^ 0 ) * (- a))) |^ m by NEWTON:11
.= (((((- 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:4
.= ((1 * (- a)) * (1 * (- a))) |^ m by PREPOWER:4
.= (a * a) |^ m
.= ((((a GeoSeq ) . 0 ) * a) * (1 * a)) |^ m by PREPOWER:4
.= ((((a GeoSeq ) . 0 ) * a) * (((a GeoSeq ) . 0 ) * a)) |^ m by PREPOWER:4
.= ((((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:11
.= ((a |^ (0 + 1)) * (a |^ (0 + 1))) |^ m by NEWTON:11
.= (a |^ (1 + 1)) |^ m by NEWTON:13
.= a |^ n by A1, NEWTON:14 ; :: thesis: verum