take L = Trivial-doubleLoopStr ; :: thesis: ( L is strict & L is Abelian & L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
thus L is strict ; :: thesis: ( L is Abelian & L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
thus L is Abelian by STRUCT_0:def 10; :: thesis: ( L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
thus L is add-associative by STRUCT_0:def 10; :: thesis: ( L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
thus L is right_zeroed by STRUCT_0:def 10; :: thesis: ( L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )
thus L is right_complementable :: thesis: ( L is associative & L is commutative & L is right_unital & L is right-distributive )
proof
let x be Element of L; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
take x ; :: according to ALGSTR_0:def 11 :: thesis: x + x = 0. L
thus x + x = 0. L by STRUCT_0:def 10; :: thesis: verum
end;
thus L is associative by STRUCT_0:def 10; :: thesis: ( L is commutative & L is right_unital & L is right-distributive )
thus L is commutative by STRUCT_0:def 10; :: thesis: ( L is right_unital & L is right-distributive )
thus L is right_unital by STRUCT_0:def 10; :: thesis: L is right-distributive
let x be Element of L; :: according to VECTSP_1:def 2 :: thesis: for b1, b2 being Element of the carrier of L holds x * (b1 + b2) = (x * b1) + (x * b2)
thus for b1, b2 being Element of the carrier of L holds x * (b1 + b2) = (x * b1) + (x * b2) by STRUCT_0:def 10; :: thesis: verum