let G be addGroup; :: thesis:
let H be strict Subgroup of G; :: thesis:
defpred S₁[ object , object ] means ex H1 being strict Subgroup of G st
( $1 = H1 & $2 = carr H1 );
A1: for x being object st x in con_class H holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in con_class H ; :: thesis:
then reconsider H = x as strict Subgroup of G by Def1;
reconsider y = carr H as set ;
take y ; :: thesis:
take H ; :: thesis:
thus ( x = H & y = carr H ) ; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A5: y in dom f and
A6: f . y = x by FUNCT_1:def 3;
consider H1 being strict Subgroup of G such that
A7: y = H1 and
A8: x = carr H1 by A2, A3, A5, A6;
carr H1, carr H are_conjugated by A2, A5, A7, Th107, ThB113;
hence x in con_class (carr H) by A8; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in con_class (carr H) ; :: thesis:
then consider B being Subset of G such that
A9: B = x and
A10: carr H,B are_conjugated ;
consider H1 being strict Subgroup of G such that
A11: the carrier of H1 = B by A10, Th93;
B = carr H1 by A11;
then A12: H1 in con_class H by A10, Th107, ThB113;
then ex H2 being strict Subgroup of G st
( H1 = H2 & f . H1 = carr H2 ) by A3;
hence x in rng f by A2, A9, A11, A12, FUNCT_1:def 3; :: thesis:

end;

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A13: ( x in dom f & y in dom f ) and
A14: f . x = f . y ; :: thesis:
( ex H1 being strict Subgroup of G st
( x = H1 & f . x = carr H1 ) & ex H2 being strict Subgroup of G st
( y = H2 & f . y = carr H2 ) ) by A2, A3, A13;
hence x = y by A14, Th59; :: thesis:

end;