let G be Abelian right-distributive doubleLoop; :: thesis: (- (1. G)) * (- (1. G)) = 1. G
thus (- (1. G)) * (- (1. G)) = - ((- (1. G)) * (1_ G)) by Th14
.= - (- (1. G)) by VECTSP_1:def 4
.= 1. G by Th15 ; :: thesis: verum