reconsider A0 = 0. X as Element of X ;
defpred S₁[ Element of X, Element of X, Element of X] means ex x, y being Element of X st
( $1 = x & $2 = y & $3 = x \ ((0. X) \ y) );
A1: for a, b being Element of X ex c being Element of X st S₁[a,b,c]

proof

let a, b be Element of X; :: thesis: ex c being Element of X st S₁[a,b,c]
reconsider x = a, y = b as Element of X ;
reconsider c = x \ ((0. X) \ y) as Element of X ;
take c ; :: thesis: S₁[a,b,c]
thus S₁[a,b,c] ; :: thesis: verum

end;

consider h being BinOp of the carrier of X such that
A2: for a, b being Element of X holds S₁[a,b,h . (a,b)] from BINOP_1:sch 3(A1);
set G = addLoopStr(# the carrier of X,h,A0 #);
A3: for x, y being Element of X holds h . (x,y) = x \ ((0. X) \ y)

proof

let x, y be Element of X; :: thesis: h . (x,y) = x \ ((0. X) \ y)
ex x9, y9 being Element of X st
( x = x9 & y = y9 & h . (x,y) = x9 \ ((0. X) \ y9) ) by A2;
hence h . (x,y) = x \ ((0. X) \ y) ; :: thesis: verum

end;

A4: for a being Element of X ex b, x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )

proof

let a be Element of X; :: thesis: ex b, x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )
reconsider x = a as Element of X ;
reconsider b = (0. X) \ x as Element of X ;
A5: b \ ((0. X) \ x) = 0. X by BCIALG_1:def 5;
take b ; :: thesis: ex x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )
x \ ((0. X) \ b) = x \ ((x `) `)
.= x \ x by BCIALG_1:54
.= 0. X by BCIALG_1:def 5 ;
hence ex x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) by A5; :: thesis: verum

end;

( addLoopStr(# the carrier of X,h,A0 #) is Abelian & addLoopStr(# the carrier of X,h,A0 #) is add-associative & addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable )

proof

thus addLoopStr(# the carrier of X,h,A0 #) is Abelian :: thesis: ( addLoopStr(# the carrier of X,h,A0 #) is add-associative & addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable )

proof

let a, b be Element of addLoopStr(# the carrier of X,h,A0 #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of X ;
thus a + b = x \ ((0. X) \ y) by A3
.= y \ ((0. X) \ x) by BCIALG_1:57
.= b + a by A3 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable )

let a, b, c be Element of addLoopStr(# the carrier of X,h,A0 #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of X ;
thus (a + b) + c = h . ((x \ ((0. X) \ y)),z) by A3
.= (x \ ((0. X) \ y)) \ ((0. X) \ z) by A3
.= (y \ ((0. X) \ x)) \ ((0. X) \ z) by BCIALG_1:57
.= (y \ ((0. X) \ z)) \ ((0. X) \ x) by BCIALG_1:7
.= x \ ((0. X) \ (y \ ((0. X) \ z))) by BCIALG_1:57
.= h . (x,(y \ ((0. X) \ z))) by A3
.= a + (b + c) by A3 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: addLoopStr(# the carrier of X,h,A0 #) is right_complementable

let a be Element of addLoopStr(# the carrier of X,h,A0 #); :: thesis: a + (0. addLoopStr(# the carrier of X,h,A0 #)) = a
reconsider x = a as Element of X ;
thus a + (0. addLoopStr(# the carrier of X,h,A0 #)) = x \ ((0. X) \ (0. X)) by A3
.= x \ (0. X) by BCIALG_1:2
.= a by BCIALG_1:2 ; :: thesis: verum

end;

let a be Element of addLoopStr(# the carrier of X,h,A0 #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
consider b being Element of X such that
A6: ex x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) by A4;
reconsider b = b as Element of addLoopStr(# the carrier of X,h,A0 #) ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. addLoopStr(# the carrier of X,h,A0 #)
thus a + b = 0. addLoopStr(# the carrier of X,h,A0 #) by A3, A6; :: thesis: verum

end;

then reconsider G = addLoopStr(# the carrier of X,h,A0 #) as strict AbGroup ;
take G ; :: thesis: ( the carrier of G = the carrier of X & ( for x, y being Element of X holds the addF of G . (x,y) = x \ ((0. X) \ y) ) & 0. G = 0. X )
thus ( the carrier of G = the carrier of X & ( for x, y being Element of X holds the addF of G . (x,y) = x \ ((0. X) \ y) ) & 0. G = 0. X ) by A3; :: thesis: verum