defpred S_{1}[ object , object ] means ex H being strict StableSubgroup of G st

( $2 = H & $1 = the carrier of H );

defpred S_{2}[ set ] means ex H being strict StableSubgroup of G st $1 = the carrier of H;

consider B being set such that

A1: for x being set holds

( x in B iff ( x in bool the carrier of G & S_{2}[x] ) )
from XFAMILY:sch 1();

A2: for x, y1, y2 being object st S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2 by Lm4;

consider f being Function such that

A3: for x, y being object holds

( [x,y] in f iff ( x in B & S_{1}[x,y] ) )
from FUNCT_1:sch 1(A2);

for x being object holds

( x in B iff ex y being object st [x,y] in f )

for y being object holds

( y in rng f iff y is strict StableSubgroup of G )_{1} being set st

for x being object holds

( x in b_{1} iff x is strict StableSubgroup of G )
; :: thesis: verum

( $2 = H & $1 = the carrier of H );

defpred S

consider B being set such that

A1: for x being set holds

( x in B iff ( x in bool the carrier of G & S

A2: for x, y1, y2 being object st S

y1 = y2 by Lm4;

consider f being Function such that

A3: for x, y being object holds

( [x,y] in f iff ( x in B & S

for x being object holds

( x in B iff ex y being object st [x,y] in f )

proof

then A7:
B = dom f
by XTUPLE_0:def 12;
let x be object ; :: thesis: ( x in B iff ex y being object st [x,y] in f )

thus ( x in B implies ex y being object st [x,y] in f ) :: thesis: ( ex y being object st [x,y] in f implies x in B )

thus x in B by A3, A6; :: thesis: verum

end;thus ( x in B implies ex y being object st [x,y] in f ) :: thesis: ( ex y being object st [x,y] in f implies x in B )

proof

given y being object such that A6:
[x,y] in f
; :: thesis: x in B
assume A4:
x in B
; :: thesis: ex y being object st [x,y] in f

then consider H being strict StableSubgroup of G such that

A5: x = the carrier of H by A1;

reconsider y = H as object ;

take y ; :: thesis: [x,y] in f

thus [x,y] in f by A3, A4, A5; :: thesis: verum

end;then consider H being strict StableSubgroup of G such that

A5: x = the carrier of H by A1;

reconsider y = H as object ;

take y ; :: thesis: [x,y] in f

thus [x,y] in f by A3, A4, A5; :: thesis: verum

thus x in B by A3, A6; :: thesis: verum

for y being object holds

( y in rng f iff y is strict StableSubgroup of G )

proof

hence
ex b
let y be object ; :: thesis: ( y in rng f iff y is strict StableSubgroup of G )

thus ( y in rng f implies y is strict StableSubgroup of G ) :: thesis: ( y is strict StableSubgroup of G implies y in rng f )

then reconsider H = y as strict StableSubgroup of G ;

reconsider x = the carrier of H as set ;

A9: y is set by TARSKI:1;

H is Subgroup of G by Def7;

then the carrier of H c= the carrier of G by GROUP_2:def 5;

then A10: x in dom f by A1, A7;

then [x,y] in f by A3, A7;

then y = f . x by A10, FUNCT_1:def 2, A9;

hence y in rng f by A10, FUNCT_1:def 3; :: thesis: verum

end;thus ( y in rng f implies y is strict StableSubgroup of G ) :: thesis: ( y is strict StableSubgroup of G implies y in rng f )

proof

assume
y is strict StableSubgroup of G
; :: thesis: y in rng f
assume
y in rng f
; :: thesis: y is strict StableSubgroup of G

then consider x being object such that

A8: ( x in dom f & y = f . x ) by FUNCT_1:def 3;

[x,y] in f by A8, FUNCT_1:def 2;

then ex H being strict StableSubgroup of G st

( y = H & x = the carrier of H ) by A3;

hence y is strict StableSubgroup of G ; :: thesis: verum

end;then consider x being object such that

A8: ( x in dom f & y = f . x ) by FUNCT_1:def 3;

[x,y] in f by A8, FUNCT_1:def 2;

then ex H being strict StableSubgroup of G st

( y = H & x = the carrier of H ) by A3;

hence y is strict StableSubgroup of G ; :: thesis: verum

then reconsider H = y as strict StableSubgroup of G ;

reconsider x = the carrier of H as set ;

A9: y is set by TARSKI:1;

H is Subgroup of G by Def7;

then the carrier of H c= the carrier of G by GROUP_2:def 5;

then A10: x in dom f by A1, A7;

then [x,y] in f by A3, A7;

then y = f . x by A10, FUNCT_1:def 2, A9;

hence y in rng f by A10, FUNCT_1:def 3; :: thesis: verum

for x being object holds

( x in b