let R be non empty unital multMagma ; :: thesis: for a being Element of R holds
( a |^ 0 = 1_ R & a |^ 1 = a )
let a be Element of R; :: thesis: ( a |^ 0 = 1_ R & a |^ 1 = a )
thus a |^ 0 = 1_ R by GROUP_1:def 8; :: thesis: a |^ 1 = a
0 + 1 = 1 ;
then (power R) . a,1 = ((power R) . a,0 ) * a by GROUP_1:def 8
.= (1_ R) * a by GROUP_1:def 8
.= a by GROUP_1:def 5 ;
hence a |^ 1 = a ; :: thesis: verum