let A, B be Point of (TOP-REAL 2); |.(A - ((1 / 2) * (A + B))).| = (1 / 2) * |.(A - B).|
|.(A - ((1 / 2) * (A + B))).| =
|.(A - (((1 / 2) * A) + ((1 / 2) * B))).|
by RLVECT_1:def 5
.=
|.((A - ((1 / 2) * A)) - ((1 / 2) * B)).|
by RLVECT_1:27
.=
|.(((1 * A) - ((1 / 2) * A)) - ((1 / 2) * B)).|
by RLVECT_1:def 8
.=
|.(((1 - (1 / 2)) * A) - ((1 / 2) * B)).|
by RLVECT_1:35
.=
|.((1 / 2) * (A - B)).|
by RLVECT_1:34
.=
|.(1 / 2).| * |.(A - B).|
by TOPRNS_1:7
.=
(1 / 2) * |.(A - B).|
by ABSVALUE:def 1
;
hence
|.(A - ((1 / 2) * (A + B))).| = (1 / 2) * |.(A - B).|
; verum