defpred S_{1}[ 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_{1}[a] } as Subset of G from DOMAIN_1:sch 7();

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

reconsider A = { a where a is Element of G : S

A1: now :: thesis: for a, b being Element of G st a in A & b in A holds

a * b in A

a * b in A

let a, b be Element of G; :: thesis: ( a in A & b in A implies a * b in A )

assume that

A2: a in A and

A3: b in A ; :: thesis: a * b in A

consider c being Element of G such that

A4: c = a and

A5: for b being Element of G holds c * b = b * c by A2;

consider d being Element of G such that

A6: d = b and

A7: for a being Element of G holds d * a = a * d by A3;

end;assume that

A2: a in A and

A3: b in A ; :: thesis: a * b in A

consider c being Element of G such that

A4: c = a and

A5: for b being Element of G holds c * b = b * c by A2;

consider d being Element of G such that

A6: d = b and

A7: for a being Element of G holds d * a = a * d by A3;

now :: thesis: for e being Element of G holds (a * b) * e = e * (a * b)

hence
a * b in A
; :: thesis: verumlet e be Element of G; :: thesis: (a * b) * e = e * (a * b)

thus (a * b) * e = a * (b * e) by GROUP_1:def 3

.= a * (e * d) by A6, A7

.= (a * e) * b by A6, GROUP_1:def 3

.= (e * c) * b by A4, A5

.= e * (a * b) by A4, GROUP_1:def 3 ; :: thesis: verum

end;thus (a * b) * e = a * (b * e) by GROUP_1:def 3

.= a * (e * d) by A6, A7

.= (a * e) * b by A6, GROUP_1:def 3

.= (e * c) * b by A4, A5

.= e * (a * b) by A4, GROUP_1:def 3 ; :: thesis: verum

A8: now :: thesis: for a being Element of G st a in A holds

a " in A

a " in A

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

A9: b = a and

A10: for c being Element of G holds b * c = c * b ;

end;assume a in A ; :: thesis: a " in A

then consider b being Element of G such that

A9: b = a and

A10: for c being Element of G holds b * c = c * b ;

now :: thesis: for c being Element of G holds (a ") * c = c * (a ")

hence
a " in A
; :: thesis: verumlet c be Element of G; :: thesis: (a ") * c = c * (a ")

thus (a ") * c = (((a ") * c) ") "

.= ((c ") * ((a ") ")) " by GROUP_1:17

.= ((c ") * b) " by A9

.= (b * (c ")) " by A10

.= (((a ") ") * (c ")) " by A9

.= ((c * (a ")) ") " by GROUP_1:17

.= c * (a ") ; :: thesis: verum

end;thus (a ") * c = (((a ") * c) ") "

.= ((c ") * ((a ") ")) " by GROUP_1:17

.= ((c ") * b) " by A9

.= (b * (c ")) " by A10

.= (((a ") ") * (c ")) " by A9

.= ((c * (a ")) ") " by GROUP_1:17

.= c * (a ") ; :: thesis: verum

now :: thesis: for b being Element of G holds (1_ G) * b = b * (1_ G)

then
1_ G in A
;let b be Element of G; :: thesis: (1_ G) * b = b * (1_ G)

(1_ G) * b = b by GROUP_1:def 4;

hence (1_ G) * b = b * (1_ G) by GROUP_1:def 4; :: thesis: verum

end;(1_ G) * b = b by GROUP_1:def 4;

hence (1_ G) * b = b * (1_ G) by GROUP_1:def 4; :: thesis: verum

hence ex b