let U be Universe; :: thesis: GroupObjects U,U are_equipotent
set GOU = GroupObjects U;
reconsider GOU9 = GroupObjects U as non empty set ;
defpred S₁[ object , object ] means ( $2 in U & GO $2,$1 );
A1: for x being Element of GOU9 ex y being Element of U st S₁[x,y]

proof

let x be Element of GOU9; :: thesis: ex y being Element of U st S₁[x,y]
ex x9 being object st
( x9 in U & GO x9,x ) by GRCAT_1:def 24;
hence ex y being Element of U st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of GOU9,U such that
A2: for x being Element of GOU9 holds S₁[x,f . x] from FUNCT_2:sch 3(A1);

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x91 = x1, x92 = x2 as Element of GroupObjects U by A3, A4, PARTFUN1:def 2;
consider y1, y2, y3, y4 being set such that
A6: f . x91 = [y1,y2,y3,y4] and
A7: ex G1 being strict AddGroup st
( x91 = G1 & y1 = the carrier of G1 & y2 = the addF of G1 & y3 = comp G1 & y4 = 0. G1 ) by A2, GRCAT_1:def 23;
consider z1, z2, z3, z4 being set such that
A8: f . x91 = [z1,z2,z3,z4] and
A9: ex G2 being strict AddGroup st
( x92 = G2 & z1 = the carrier of G2 & z2 = the addF of G2 & z3 = comp G2 & z4 = 0. G2 ) by A5, A2, GRCAT_1:def 23;
consider G1 being strict AddGroup such that
A10: ( x91 = G1 & y1 = the carrier of G1 & y2 = the addF of G1 & y3 = comp G1 & y4 = 0. G1 ) by A7;
consider G2 being strict AddGroup such that
A11: ( x92 = G2 & z1 = the carrier of G2 & z2 = the addF of G2 & z3 = comp G2 & z4 = 0. G2 ) by A9;
( the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 & 0. G1 = 0. G2 & the ZeroF of G1 = 0. G1 & the ZeroF of G2 = 0. G2 ) by A10, A11, STRUCT_0:def 6, XTUPLE_0:5, A8, A6;
hence x1 = x2 by A10, A11; :: thesis: verum

end;

then A12: f is one-to-one by FUNCT_1:def 4;
reconsider U9 = U as non empty set ;
deffunc H₁( object ) -> non empty addLoopStr = Trivial-addLoopStr $1;
A13: for x being object st x in U holds
H₁(x) in GroupObjects U by Th82;
consider g being Function of U,(GroupObjects U) such that
A14: for x being object st x in U holds
g . x = H₁(x) from FUNCT_2:sch 2(A13);

now :: thesis: for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume that
A15: x1 in dom g and
A16: x2 in dom g and
A17: g . x1 = g . x2 ; :: thesis: x1 = x2
reconsider x91 = x1, x92 = x2 as Element of U by A15, A16, PARTFUN1:def 2;
( g . x91 = Trivial-addLoopStr x91 & g . x92 = Trivial-addLoopStr x92 ) by A14;
hence x1 = x2 by A17; :: thesis: verum

end;

then g is one-to-one by FUNCT_1:def 4;
hence GroupObjects U,U are_equipotent by A12, KNASTER:12; :: thesis: verum