let G be addGroup; :: thesis:
defpred S₁[ object , object ] means ex H being strict Subgroup of G st
( $1 = H & $2 = the carrier of H );
assume A1: G is finite ; :: thesis:
A2: for x being object st x in Subgroups G holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in Subgroups G ; :: thesis:
then reconsider F = x as strict Subgroup of G by Def1;
reconsider y = the carrier of F as set ;
take y ; :: thesis:
take F ; :: thesis:
thus ( x = F & y = the carrier of F ) ; :: thesis:

end;

consider f being Function such that
A3: dom f = Subgroups G and
A4: for x being object st x in Subgroups G holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
A5: rng f c= bool the carrier of G

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A6: ( y in dom f & f . y = x ) by FUNCT_1:def 3;
consider H being strict Subgroup of G such that
y = H and
A7: x = the carrier of H by A3, A4, A6;
the carrier of H c= the carrier of G by DefA5;
hence x in bool the carrier of G by A7; :: thesis:

end;

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

end;