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 b₁, b₂ being Element of the carrier of L holds x * (b₁ + b₂) = (x * b₁) + (x * b₂)
thus for b₁, b₂ being Element of the carrier of L holds x * (b₁ + b₂) = (x * b₁) + (x * b₂) by STRUCT_0:def 10; :: thesis: verum