let G be Group; :: thesis: for A being Subset of G holds A |^ (1_ G) = A
let A be Subset of G; :: thesis: A |^ (1_ G) = A
thus A |^ (1_ G) = (((1_ G) " ) * A) * (1_ G) by Th59
.= ((1_ G) " ) * A by GROUP_2:43
.= (1_ G) * A by GROUP_1:16
.= A by GROUP_2:43 ; :: thesis: verum