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 13
.= (x + x) + ((- y) + (- y)) by RLVECT_1:45
.= x + (x + ((- y) + (- y))) by RLVECT_1:def 6
.= x + ((x + (- y)) + (- y)) by RLVECT_1:def 6
.= (x + (- y)) + (x + (- y)) by RLVECT_1:def 6 ;
then (- y) + x = 0. G by VECTSP_1:def 30;
hence x = - (- y) by RLVECT_1:19
.= y by RLVECT_1:30 ;
:: thesis: verum