let x, y1, y2 be object ; ( GO x,y1 & GO x,y2 implies y1 = y2 )
assume that
A1:
GO x,y1
and
A2:
GO x,y2
; y1 = y2
consider a1, a2, a3, a4 being set such that
A3:
x = [a1,a2,a3,a4]
and
A4:
ex G being strict AddGroup st
( y1 = G & a1 = the carrier of G & a2 = the addF of G & a3 = comp G & a4 = 0. G )
by A1;
consider G1 being strict AddGroup such that
A5:
y1 = G1
and
A6:
( a1 = the carrier of G1 & a2 = the addF of G1 )
and
a3 = comp G1
and
A7:
a4 = 0. G1
by A4;
consider b1, b2, b3, b4 being set such that
A8:
x = [b1,b2,b3,b4]
and
A9:
ex G being strict AddGroup st
( y2 = G & b1 = the carrier of G & b2 = the addF of G & b3 = comp G & b4 = 0. G )
by A2;
consider G2 being strict AddGroup such that
A10:
y2 = G2
and
A11:
( b1 = the carrier of G2 & b2 = the addF of G2 )
and
b3 = comp G2
and
A12:
b4 = 0. G2
by A9;
( the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 )
by A3, A8, A6, A11, XTUPLE_0:5;
hence
y1 = y2
by A3, A8, A5, A7, A10, A12, XTUPLE_0:5; verum