let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; :: thesis: for x, y being Element of G holds

( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )

let x, y be Element of G; :: thesis: ( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )

Double (0. G) = 0. G by RLVECT_1:def 4;

hence Half (0. G) = 0. G by Def6; :: thesis: ( Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )

Double ((Half x) + (Half y)) = (Double (Half x)) + (Double (Half y)) by Th10

.= x + (Double (Half y)) by Def6

.= x + y by Def6 ;

hence Half (x + y) = (Half x) + (Half y) by Def6; :: thesis: ( ( Half x = Half y implies x = y ) & Half (Double x) = x )

thus ( Half x = Half y implies x = y ) :: thesis: Half (Double x) = x

( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )

let x, y be Element of G; :: thesis: ( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )

Double (0. G) = 0. G by RLVECT_1:def 4;

hence Half (0. G) = 0. G by Def6; :: thesis: ( Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )

Double ((Half x) + (Half y)) = (Double (Half x)) + (Double (Half y)) by Th10

.= x + (Double (Half y)) by Def6

.= x + y by Def6 ;

hence Half (x + y) = (Half x) + (Half y) by Def6; :: thesis: ( ( Half x = Half y implies x = y ) & Half (Double x) = x )

thus ( Half x = Half y implies x = y ) :: thesis: Half (Double x) = x

proof

thus
Half (Double x) = x
by Def6; :: thesis: verum
assume
Half x = Half y
; :: thesis: x = y

hence x = Double (Half y) by Def6

.= y by Def6 ;

:: thesis: verum

end;hence x = Double (Half y) by Def6

.= y by Def6 ;

:: thesis: verum