set L = doubleLoopStr(# A,od0,om0,nm,nd #);
A1: 0. doubleLoopStr(# A,od0,om0,nm,nd #) = nd ;
1. doubleLoopStr(# A,od0,om0,nm,nd #) = nm ;
then reconsider L = doubleLoopStr(# A,od0,om0,nm,nd #) as non degenerated doubleLoopStr by A1, Lm3, Lm4, STRUCT_0:def 8;
take L ; :: thesis: ( L is strict & L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable )
thus L is strict ; :: thesis: ( L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable )
thus the multF of L is the carrier of L \ {(0. L)} -subsetpreserving by Lm28; :: according to REALSET2:def 4 :: thesis: ( ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable )
L is right_complementable
proof
let a be Element of L; :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
take a ; :: according to ALGSTR_0:def 11 :: thesis: a + a = 0. L
( a = In (0,2) or a = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def 2;
hence a + a = 0. L by Lm8, Lm11; :: thesis: verum
end;
hence ( ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable ) by Lm23, Lm24, Lm25, Lm26, Lm27; :: thesis: verum