let x, y1, y2 be set ; :: 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, 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, Def16;
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, Def16;
consider G1 being strict Ring such that
A7: ( y1 = G1 & a1 = the carrier of G1 & a2 = the addF of G1 & a3 = comp G1 & a4 = 0. G1 & a5 = the multF of G1 & a6 = 1. G1 ) by A4;
consider G2 being strict Ring such that
A8: ( y2 = G2 & b1 = the carrier of G2 & b2 = the addF of G2 & b3 = comp G2 & b4 = 0. G2 & b5 = the multF of G2 & b6 = 1. G2 ) by A6;
( [a1,a2,a3,a4] = [b1,b2,b3,b4] & a5 = b5 & a6 = b6 ) by A3, A5, MCART_1:28;
then ( the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 & comp G1 = comp G2 & 0. G1 = 0. G2 & the multF of G1 = the multF of G2 & 1. G1 = 1. G2 ) by A7, A8, MCART_1:33;
hence y1 = y2 by A7, A8; :: thesis: verum