let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a being Element of R holds - (a |^ p) = (- a) |^ p
let R be commutative p -characteristic Ring; :: thesis: for a being Element of R holds - (a |^ p) = (- a) |^ p
let a be Element of R; :: thesis: - (a |^ p) = (- a) |^ p
((- a) |^ p) - (- (a |^ p)) = ((- a) + a) |^ p by fresh
.= (0. R) |^ p by RLVECT_1:5
.= 0. R ;
hence - (a |^ p) = (- a) |^ p by RLVECT_1:21; :: thesis: verum