reconsider A0 = 0. X as Element of X ;

defpred S_{1}[ 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_{1}[a,b,c]

A2: for a, b being Element of X holds S_{1}[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)

( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )

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

defpred S

( $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

proof

consider h being BinOp of the carrier of X such that
let a, b be Element of X; :: thesis: ex c being Element of X st S_{1}[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_{1}[a,b,c]

thus S_{1}[a,b,c]
; :: thesis: verum

end;reconsider x = a, y = b as Element of X ;

reconsider c = x \ ((0. X) \ y) as Element of X ;

take c ; :: thesis: S

thus S

A2: for a, b being Element of X holds S

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

A4:
for a being Element of X ex b, x being Element of X st
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;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

( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )

proof

( 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 )
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;( 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

proof

then reconsider G = addLoopStr(# the carrier of X,h,A0 #) as strict AbGroup ;
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 )

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;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;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

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;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

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 #); :: according to ALGSTR_0:def 16 :: thesis: a 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;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

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

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