let R be Ring; :: thesis: for x, y1, y2 being object st GO x,y1,R & GO x,y2,R holds
y1 = y2
let x, y1, y2 be object ; :: 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 object 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 ZeroF of G #) & a2 = the lmult of G ) by A1;
consider G1 being strict LeftMod of R such that
A5: y1 = G1 and
A6: a1 = addLoopStr(# the carrier of G1, the addF of G1, the ZeroF of G1 #) and
A7: a2 = the lmult of G1 by A4;
consider b1, b2 being object such that
A8: x = [b1,b2] and
A9: ex G being strict LeftMod of R st
( y2 = G & b1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & b2 = the lmult of G ) by A2;
consider G2 being strict LeftMod of R such that
A10: y2 = G2 and
A11: b1 = addLoopStr(# the carrier of G2, the addF of G2, the ZeroF of G2 #) and
A12: b2 = the lmult of G2 by A9;
addLoopStr(# the carrier of G1, the addF of G1, the ZeroF of G1 #) = addLoopStr(# the carrier of G2, the addF of G2, the ZeroF of G2 #) by A3, A8, A6, A11, XTUPLE_0:1;
hence y1 = y2 by A3, A8, A5, A7, A10, A12, XTUPLE_0:1; :: thesis: verum