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, a5, a6 being set such that
A3:
x = [[a1,a2,a3,a4],a5,a6]
and
A4:
ex G being strict Ring st
( y1 = G & a1 = the carrier of G & a2 = the addF of G & a3 = comp G & a4 = 0. G & a5 = the multF of G & a6 = 1. G )
by A1;
consider b1, b2, b3, b4, b5, b6 being set such that
A5:
x = [[b1,b2,b3,b4],b5,b6]
and
A6:
ex G being strict Ring st
( y2 = G & b1 = the carrier of G & b2 = the addF of G & b3 = comp G & b4 = 0. G & b5 = the multF of G & b6 = 1. G )
by A2;
consider G2 being strict Ring such that
A7:
y2 = G2
and
A8:
( b1 = the carrier of G2 & b2 = the addF of G2 )
and
b3 = comp G2
and
A9:
b4 = 0. G2
and
A10:
( b5 = the multF of G2 & b6 = 1. G2 )
by A6;
consider G1 being strict Ring such that
A11:
y1 = G1
and
A12:
( a1 = the carrier of G1 & a2 = the addF of G1 )
and
a3 = comp G1
and
A13:
a4 = 0. G1
and
A14:
( a5 = the multF of G1 & a6 = 1. G1 )
by A4;
A15:
( the multF of G1 = the multF of G2 & 1. G1 = 1. G2 )
by A3, A5, A14, A10, XTUPLE_0:3;
A16:
[a1,a2,a3,a4] = [b1,b2,b3,b4]
by A3, A5, XTUPLE_0:3;
then
( the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 )
by A12, A8, XTUPLE_0:5;
hence
y1 = y2
by A11, A13, A7, A9, A16, A15, XTUPLE_0:5; verum