set X = { g where g is Element of G : (T ^ g) .: A = A } ;

now :: thesis: for x being object st x in { g where g is Element of G : (T ^ g) .: A = A } holds
x in the carrier of G

let x be object ; :: thesis: ( x in { g where g is Element of G : (T ^ g) .: A = A } implies x in the carrier of G )
assume x in { g where g is Element of G : (T ^ g) .: A = A } ; :: thesis: x in the carrier of G
then ex g being Element of G st
( x = g & (T ^ g) .: A = A ) ;
hence x in the carrier of G ; :: thesis: verum

end;

then reconsider X = { g where g is Element of G : (T ^ g) .: A = A } as Subset of G by TARSKI:def 3;
A1: for g1, g2 being Element of G st g1 in X & g2 in X holds
g1 * g2 in X

proof

let g1, g2 be Element of G; :: thesis: ( g1 in X & g2 in X implies g1 * g2 in X )
assume g1 in X ; :: thesis: ( not g2 in X or g1 * g2 in X )
then A2: ex g being Element of G st
( g = g1 & (T ^ g) .: A = A ) ;
assume g2 in X ; :: thesis: g1 * g2 in X
then A3: ex g being Element of G st
( g = g2 & (T ^ g) .: A = A ) ;
(T ^ (g1 * g2)) .: A = ((T ^ g1) * (T ^ g2)) .: A by Def1
.= A by A2, A3, RELAT_1:126 ;
hence g1 * g2 in X ; :: thesis: verum

end;

A4: (id E) .: A = A by FUNCT_1:92;
A5: for g being Element of G st g in X holds
g " in X

proof

let g be Element of G; :: thesis: ( g in X implies g " in X )
assume g in X ; :: thesis: g " in X
then ex g9 being Element of G st
( g9 = g & (T ^ g9) .: A = A ) ;
then (T ^ (g ")) .: A = ((T ^ (g ")) * (T ^ g)) .: A by RELAT_1:126
.= (T ^ ((g ") * g)) .: A by Def1
.= (T ^ (1_ G)) .: A by GROUP_1:def 5
.= A by A4, Def1 ;
hence g " in X ; :: thesis: verum

end;

(T ^ (1_ G)) .: A = A by A4, Def1;
then 1_ G in X ;
hence ex b₁ being strict Subgroup of G st the carrier of b₁ = { g where g is Element of G : (T ^ g) .: A = A } by A1, A5, GROUP_2:52; :: thesis: verum