let G be Group; :: thesis: for a being Element of G holds

( ((1). G) * a = {a} & a * ((1). G) = {a} )

let a be Element of G; :: thesis: ( ((1). G) * a = {a} & a * ((1). G) = {a} )

A1: the carrier of ((1). G) = {(1_ G)} by Def7;

hence ((1). G) * a = {((1_ G) * a)} by Th18

.= {a} by GROUP_1:def 4 ;

:: thesis: a * ((1). G) = {a}

thus a * ((1). G) = {(a * (1_ G))} by A1, Th18

.= {a} by GROUP_1:def 4 ; :: thesis: verum

( ((1). G) * a = {a} & a * ((1). G) = {a} )

let a be Element of G; :: thesis: ( ((1). G) * a = {a} & a * ((1). G) = {a} )

A1: the carrier of ((1). G) = {(1_ G)} by Def7;

hence ((1). G) * a = {((1_ G) * a)} by Th18

.= {a} by GROUP_1:def 4 ;

:: thesis: a * ((1). G) = {a}

thus a * ((1). G) = {(a * (1_ G))} by A1, Th18

.= {a} by GROUP_1:def 4 ; :: thesis: verum