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

proof

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

end;

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