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 :: 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 )

proof

let x be Element of L; :: according to RLVECT_1:def 2 :: thesis: for b₁ being Element of the carrier of L holds x + b₁ = b₁ + x
thus for b₁ being Element of the carrier of L holds x + b₁ = b₁ + x by STRUCT_0:def 10; :: thesis: verum

end;

thus L is add-associative :: thesis: ( L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )

proof

let x be Element of L; :: according to RLVECT_1:def 3 :: thesis: for b₁, b₂ being Element of the carrier of L holds (x + b₁) + b₂ = x + (b₁ + b₂)
thus for b₁, b₂ being Element of the carrier of L holds (x + b₁) + b₂ = x + (b₁ + b₂) by STRUCT_0:def 10; :: thesis: verum

end;

thus L is right_zeroed :: thesis: ( L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive )

proof

let x be Element of L; :: according to RLVECT_1:def 4 :: thesis: x + (0. L) = x
thus x + (0. L) = x by STRUCT_0:def 10; :: thesis: verum

end;

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 :: thesis: ( L is commutative & L is right_unital & L is right-distributive )

proof

let x be Element of L; :: according to GROUP_1:def 3 :: thesis: for b₁, b₂ being Element of the carrier of L holds (x * b₁) * b₂ = x * (b₁ * b₂)
thus for b₁, b₂ being Element of the carrier of L holds (x * b₁) * b₂ = x * (b₁ * b₂) by STRUCT_0:def 10; :: thesis: verum

end;

thus L is commutative :: thesis: ( L is right_unital & L is right-distributive )

proof

let x be Element of L; :: according to GROUP_1:def 12 :: thesis: for b₁ being Element of the carrier of L holds x * b₁ = b₁ * x
thus for b₁ being Element of the carrier of L holds x * b₁ = b₁ * x by STRUCT_0:def 10; :: thesis: verum

end;

thus L is right_unital :: thesis: L is right-distributive

proof

let x be Element of L; :: according to VECTSP_1:def 4 :: thesis: x * (1. L) = x
thus x * (1. L) = x by STRUCT_0:def 10; :: thesis: verum

end;

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