defpred S₁[ Element of G] means for b being Element of G holds $1 * b = b * $1;
reconsider A = { a where a is Element of G : S₁[a] } as Subset of G from DOMAIN_1:sch 7();

now

let b be Element of G; :: thesis: (1_ G) * b = b * (1_ G)
( (1_ G) * b = b & b * (1_ G) = b ) by GROUP_1:def 5;
hence (1_ G) * b = b * (1_ G) ; :: thesis: verum

end;

then A1: 1_ G in A ;

A2: now

let a, b be Element of G; :: thesis: ( a in A & b in A implies a * b in A )
assume that
A3: a in A and
A4: b in A ; :: thesis: a * b in A
consider c being Element of G such that
A5: ( c = a & ( for b being Element of G holds c * b = b * c ) ) by A3;
consider d being Element of G such that
A6: ( d = b & ( for a being Element of G holds d * a = a * d ) ) by A4;

now

let e be Element of G; :: thesis: (a * b) * e = e * (a * b)
thus (a * b) * e = a * (b * e) by GROUP_1:def 4
.= a * (e * d) by A6
.= (a * e) * b by A6, GROUP_1:def 4
.= (e * c) * b by A5
.= e * (a * b) by A5, GROUP_1:def 4 ; :: thesis: verum

end;

hence a * b in A ; :: thesis: verum

end;

now

let a be Element of G; :: thesis: ( a in A implies a " in A )
assume a in A ; :: thesis: a " in A
then consider b being Element of G such that
A7: ( b = a & ( for c being Element of G holds b * c = c * b ) ) ;

now

let c be Element of G; :: thesis: (a " ) * c = c * (a " )
thus (a " ) * c = (((a " ) * c) " ) "
.= ((c " ) * ((a " ) " )) " by GROUP_1:25
.= ((c " ) * b) " by A7
.= (b * (c " )) " by A7
.= (((a " ) " ) * (c " )) " by A7
.= ((c * (a " )) " ) " by GROUP_1:25
.= c * (a " ) ; :: thesis: verum

end;

hence a " in A ; :: thesis: verum

end;

hence ex b₁ being strict Subgroup of G st the carrier of b₁ = { a where a is Element of G : for b being Element of G holds a * b = b * a } by A1, A2, GROUP_2:61; :: thesis: verum