let G be Group; :: thesis: for A being Subset of G st A <> {} holds
(1_ G) |^ A = {(1_ G)}
let A be Subset of G; :: thesis: ( A <> {} implies (1_ G) |^ A = {(1_ G)} )
set y = the Element of A;
assume A1: A <> {} ; :: thesis: (1_ G) |^ A = {(1_ G)}
then reconsider y = the Element of A as Element of G by TARSKI:def 3;
thus (1_ G) |^ A c= {(1_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(1_ G)} c= (1_ G) |^ A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (1_ G) |^ A or x in {(1_ G)} )
assume x in (1_ G) |^ A ; :: thesis: x in {(1_ G)}
then ex a being Element of G st
( x = (1_ G) |^ a & a in A ) by Th42;
then x = 1_ G by Th17;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1_ G)} or x in (1_ G) |^ A )
assume x in {(1_ G)} ; :: thesis: x in (1_ G) |^ A
then x = 1_ G by TARSKI:def 1;
then (1_ G) |^ y = x by Th17;
hence x in (1_ G) |^ A by A1, Th42; :: thesis: verum