let F be Field; :: thesis: addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) is AbGroup
set L = addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #);
A1: addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) is Abelian

proof

let v, w be Element of addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #); :: according to RLVECT_1:def 5 :: thesis: v + w = w + v
reconsider a = v, b = w as Element of F ;
thus v + w = a + b
.= b + a
.= w + v ; :: thesis: verum

end;

A2: addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) is add-associative

proof

let u, v, w be Element of addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #); :: according to RLVECT_1:def 6 :: thesis: (u + v) + w = u + (v + w)
reconsider a = u, b = v, c = w as Element of F ;
thus (u + v) + w = (a + b) + c
.= a + (b + c) by RLVECT_1:def 6
.= u + (v + w) ; :: thesis: verum

end;

A3: addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) is right_zeroed

proof

let v be Element of addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #); :: according to RLVECT_1:def 7 :: thesis: v + (0. addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #)) = v
reconsider a = v as Element of F ;
thus v + (0. addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #)) = a + (0. F)
.= v by RLVECT_1:def 7 ; :: thesis: verum

end;

addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) is right_complementable

proof

let v be Element of addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider a = v as Element of F ;
consider b being Element of F such that
A4: a + b = 0. F by ALGSTR_0:def 11;
reconsider w = b as Element of addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #)
thus v + w = 0. addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) by A4; :: thesis: verum

end;

hence addLoopStr(# the carrier of F,the addF of F,the ZeroF of F #) is AbGroup by A1, A2, A3; :: thesis: verum