let ADG be Uniquely_Two_Divisible_Group; :: thesis: for a, b, c, b9 being Element of ADG st a,b ==> b,c & a,b9 ==> b9,c holds
b = b9
let a, b, c, b9 be Element of ADG; :: thesis: ( a,b ==> b,c & a,b9 ==> b9,c implies b = b9 )
assume ( a,b ==> b,c & a,b9 ==> b9,c ) ; :: thesis: b = b9
then ( a + c = b + b & a + c = b9 + b9 ) by Th5;
then (b + (- b9)) + b = (b9 + b9) + (- b9) by RLVECT_1:def 3
.= b9 + (b9 + (- b9)) by RLVECT_1:def 3
.= b9 + (0. ADG) by RLVECT_1:5
.= b9 by RLVECT_1:4 ;
then A1: (b + (- b9)) + (b + (- b9)) = b9 + (- b9) by RLVECT_1:def 3
.= 0. ADG by RLVECT_1:5 ;
b9 = (0. ADG) + b9 by RLVECT_1:4
.= (b + (- b9)) + b9 by A1, VECTSP_1:def 18
.= b + ((- b9) + b9) by RLVECT_1:def 3
.= b + (0. ADG) by RLVECT_1:5
.= b by RLVECT_1:4 ;
hence b = b9 ; :: thesis: verum