let x, y1, y2 be object ; :: thesis: ( GO x,y1 & GO x,y2 implies y1 = y2 )
assume that
A1: GO x,y1 and
A2: GO x,y2 ; :: thesis: 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; :: thesis: verum