theorem :: REALSET2:1

for F being Field holds addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is AbGroup