let G be Abelian left-distributive doubleLoop; :: thesis: (- (1. G)) * (- (1. G)) = 1. G
thus (- (1. G)) * (- (1. G)) = - ((1_ G) * (- (1. G))) by Th21
.= - (- (1. G)) by VECTSP_1:def 19
.= 1. G by Th15 ; :: thesis: verum