let G be non empty right_complementable Fanoian Abelian add-associative right_zeroed addLoopStr ; :: thesis: for x, y being Element of G st Double x = Double y holds
x = y
let x, y be Element of G; :: thesis: ( Double x = Double y implies x = y )
assume Double x = Double y ; :: thesis: x = y
then 0. G = (x + x) + (- (y + y)) by RLVECT_1:def 10
.= (x + x) + ((- y) + (- y)) by RLVECT_1:31
.= x + (x + ((- y) + (- y))) by RLVECT_1:def 3
.= x + ((x + (- y)) + (- y)) by RLVECT_1:def 3
.= (x + (- y)) + (x + (- y)) by RLVECT_1:def 3 ;
then (- y) + x = 0. G by VECTSP_1:def 18;
hence x = - (- y) by RLVECT_1:6
.= y by RLVECT_1:17 ;
:: thesis: verum