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 7; :: thesis: a |^ 1 = a
0 + 1 = 1 ;
then (power R) . (a,1) = ((power R) . (a,0)) * a by GROUP_1:def 7
.= (1_ R) * a by GROUP_1:def 7
.= a by GROUP_1:def 4 ;
hence a |^ 1 = a ; :: thesis: verum