let G be addGroup; :: thesis: for a, b being Element of G holds
( (a + b) + (- b) = a & (a + (- b)) + b = a & ((- b) + b) + a = a & (b + (- b)) + a = a & a + (b + (- b)) = a & a + ((- b) + b) = a & (- b) + (b + a) = a & b + ((- b) + a) = a )
let a, b be Element of G; :: thesis: ( (a + b) + (- b) = a & (a + (- b)) + b = a & ((- b) + b) + a = a & (b + (- b)) + a = a & a + (b + (- b)) = a & a + ((- b) + b) = a & (- b) + (b + a) = a & b + ((- b) + a) = a )
thus A1: (a + b) + (- b) = a + (b + (- b)) by RLVECT_1:def 3
.= a + (0_ G) by Def5
.= a by Def4 ; :: thesis: ( (a + (- b)) + b = a & ((- b) + b) + a = a & (b + (- b)) + a = a & a + (b + (- b)) = a & a + ((- b) + b) = a & (- b) + (b + a) = a & b + ((- b) + a) = a )
thus A2: (a + (- b)) + b = a + ((- b) + b) by RLVECT_1:def 3
.= a + (0_ G) by Def5
.= a by Def4 ; :: thesis: ( ((- b) + b) + a = a & (b + (- b)) + a = a & a + (b + (- b)) = a & a + ((- b) + b) = a & (- b) + (b + a) = a & b + ((- b) + a) = a )
thus A3: ((- b) + b) + a = (0_ G) + a by Def5
.= a by Def4 ; :: thesis: ( (b + (- b)) + a = a & a + (b + (- b)) = a & a + ((- b) + b) = a & (- b) + (b + a) = a & b + ((- b) + a) = a )
thus (b + (- b)) + a = (0_ G) + a by Def5
.= a by Def4 ; :: thesis: ( a + (b + (- b)) = a & a + ((- b) + b) = a & (- b) + (b + a) = a & b + ((- b) + a) = a )
hence ( a + (b + (- b)) = a & a + ((- b) + b) = a & (- b) + (b + a) = a & b + ((- b) + a) = a ) by A1, A2, A3, RLVECT_1:def 3; :: thesis: verum