let L be non degenerated doubleLoopStr ; :: thesis:
assume A1: ( L is add-associative & L is right_zeroed & L is right_complementable & L is Abelian & L is commutative & L is associative & L is well-unital & L is distributive & L is almost_left_invertible ) ; :: thesis:
set B = NonZero L;
A3: for y being set st y in [:(NonZero L),(NonZero L):] holds
the multF of L . y in NonZero L

proof

let z be set ; :: thesis:
assume z in [:(NonZero L),(NonZero L):] ; :: thesis:
then consider x, y being set such that
A4: ( x in NonZero L & y in NonZero L ) and
A5: z = [x,y] by ZFMISC_1:103;
reconsider x = x, y = y as Element of L by A4;
( not x in {(0. L)} & not y in {(0. L)} ) by A4, XBOOLE_0:def 5;
then ( x <> 0. L & y <> 0. L ) by TARSKI:def 1;
then x * y <> 0. L by A1, VECTSP_1:44;
then not x * y in {(0. L)} by TARSKI:def 1;
hence the multF of L . z in NonZero L by A5, XBOOLE_0:def 5; :: thesis:

end;

hence the multF of L is DnT of 0. L,the carrier of L by REALSET1:def 8; :: according to REALSET2:def 11 :: thesis:
reconsider om = the multF of L as DnT of 0. L,the carrier of L by A3, REALSET1:def 8;
let B be non empty set ; :: thesis:
let P be BinOp of B; :: thesis:
let e be Element of B; :: thesis:
assume that
A6: B = NonZero L and
A7: e = 1. L and
A8: P = the multF of L || (NonZero L) ; :: thesis:
set K = addLoopStr(# B,P,e #);
A9: addLoopStr(# B,P,e #) is Abelian

proof

let v, w be Element of addLoopStr(# B,P,e #); :: according to RLVECT_1:def 5 :: thesis:
reconsider a = v, b = w as Element of L by A6, XBOOLE_0:def 5;
A10: [v,w] in [:B,B:] ;
A11: [w,v] in [:B,B:] ;
thus v + w = a * b by A6, A8, A10, FUNCT_1:72
.= b * a by A1, GROUP_1:def 16
.= w + v by A6, A8, A11, FUNCT_1:72 ; :: thesis:

end;

A12: addLoopStr(# B,P,e #) is add-associative

proof

let u, v, w be Element of addLoopStr(# B,P,e #); :: according to RLVECT_1:def 6 :: thesis:
reconsider a = u, b = v, c = w as Element of L by A6, XBOOLE_0:def 5;
A13: [u,v] in [:B,B:] ;
then P . u,v in B by FUNCT_2:7;
then A14: [((om || B) . u,v),w] in [:B,B:] by A6, A8, ZFMISC_1:106;
A15: [v,w] in [:B,B:] ;
then P . v,w in B by FUNCT_2:7;
then A16: [u,((om || B) . v,w)] in [:B,B:] by A6, A8, ZFMISC_1:106;
thus (u + v) + w = om . ((om || B) . u,v),w by A6, A8, A14, FUNCT_1:72
.= (a * b) * c by A13, FUNCT_1:72
.= a * (b * c) by A1, GROUP_1:def 4
.= om . u,((om || B) . v,w) by A15, FUNCT_1:72
.= u + (v + w) by A6, A8, A16, FUNCT_1:72 ; :: thesis:

end;

A17: addLoopStr(# B,P,e #) is right_zeroed

proof

let v be Element of addLoopStr(# B,P,e #); :: according to RLVECT_1:def 7 :: thesis:
reconsider a = v as Element of L by A6, XBOOLE_0:def 5;
[v,(0. addLoopStr(# B,P,e #))] in [:B,B:] ;
hence v + (0. addLoopStr(# B,P,e #)) = a * (1. L) by A6, A7, A8, FUNCT_1:72
.= v by A1, VECTSP_1:def 16 ;
:: thesis:

end;

addLoopStr(# B,P,e #) is right_complementable

proof

let v be Element of addLoopStr(# B,P,e #); :: according to ALGSTR_0:def 16 :: thesis:
reconsider a = v as Element of L by A6, XBOOLE_0:def 5;
not a in {(0. L)} by A6, XBOOLE_0:def 5;
then a <> 0. L by TARSKI:def 1;
then consider b being Element of L such that
A18: b * a = 1. L by A1, VECTSP_1:def 20;
A19: a * b = 1. L by A1, A18, GROUP_1:def 16;
then b <> 0. L by A1, VECTSP_1:36;
then not b in {(0. L)} by TARSKI:def 1;
then reconsider w = b as Element of addLoopStr(# B,P,e #) by A6, XBOOLE_0:def 5;
take w ; :: according to ALGSTR_0:def 11 :: thesis:
[v,w] in [:B,B:] ;
hence v + w = 0. addLoopStr(# B,P,e #) by A6, A7, A8, A19, FUNCT_1:72; :: thesis:

end;

hence addLoopStr(# B,P,e #) is AbGroup by A9, A12, A17; :: thesis: