let A be Point of (TOP-REAL 2); :: thesis: the_midpoint_of_the_segment (A,A) = A

the_midpoint_of_the_segment (A,A) = (1 / 2) * (A + A) by Th22

.= ((1 / 2) * A) + ((1 / 2) * A) by RVSUM_1:51

.= ((1 / 2) + (1 / 2)) * A by RVSUM_1:50

.= A by RVSUM_1:52 ;

hence the_midpoint_of_the_segment (A,A) = A ; :: thesis: verum

the_midpoint_of_the_segment (A,A) = (1 / 2) * (A + A) by Th22

.= ((1 / 2) * A) + ((1 / 2) * A) by RVSUM_1:51

.= ((1 / 2) + (1 / 2)) * A by RVSUM_1:50

.= A by RVSUM_1:52 ;

hence the_midpoint_of_the_segment (A,A) = A ; :: thesis: verum