let R be Ring; :: thesis: for x, y1, y2 being set st GO x,y1,R & GO x,y2,R holds
y1 = y2
let x, y1, y2 be set ; :: thesis: ( GO x,y1,R & GO x,y2,R implies y1 = y2 )
assume that
A1: GO x,y1,R and
A2: GO x,y2,R ; :: thesis: y1 = y2
consider a1, a2 being set such that
A3: x = [a1,a2] and
A4: ex G being strict LeftMod of R st
( y1 = G & a1 = addLoopStr(# the carrier of G,the addF of G,the U2 of G #) & a2 = the lmult of G ) by A1, Def5;
consider b1, b2 being set such that
A5: x = [b1,b2] and
A6: ex G being strict LeftMod of R st
( y2 = G & b1 = addLoopStr(# the carrier of G,the addF of G,the U2 of G #) & b2 = the lmult of G ) by A2, Def5;
consider G1 being strict LeftMod of R such that
A7: ( y1 = G1 & a1 = addLoopStr(# the carrier of G1,the addF of G1,the U2 of G1 #) & a2 = the lmult of G1 ) by A4;
consider G2 being strict LeftMod of R such that
A8: ( y2 = G2 & b1 = addLoopStr(# the carrier of G2,the addF of G2,the U2 of G2 #) & b2 = the lmult of G2 ) by A6;
( addLoopStr(# the carrier of G1,the addF of G1,the U2 of G1 #) = addLoopStr(# the carrier of G2,the addF of G2,the U2 of G2 #) & the lmult of G1 = the lmult of G2 ) by A3, A5, A7, A8, ZFMISC_1:33;
hence y1 = y2 by A7, A8; :: thesis: verum