let A be non empty set ; :: thesis: RRing A is commutative Ring
A1: RRing A is Abelian

proof

let x be Element of (RRing A); :: according to RLVECT_1:def 2 :: thesis: for b₁ being Element of the carrier of (RRing A) holds x + b₁ = b₁ + x
thus for b₁ being Element of the carrier of (RRing A) holds x + b₁ = b₁ + x by Th42; :: thesis: verum

end;

A2: RRing A is add-associative

proof

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

end;

A3: RRing A is right_complementable

proof

let x be Element of (RRing A); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
consider t being Element of (RRing A) such that
A4: x + t = 0. (RRing A) by Th42;
take t ; :: according to ALGSTR_0:def 11 :: thesis: x + t = 0. (RRing A)
thus x + t = 0. (RRing A) by A4; :: thesis: verum

end;

A5: RRing A is right_zeroed

proof

let x be Element of (RRing A); :: according to RLVECT_1:def 4 :: thesis: x + (0. (RRing A)) = x
thus x + (0. (RRing A)) = x by Th42; :: thesis: verum

end;

A6: RRing A is distributive

proof

let x be Element of (RRing A); :: according to VECTSP_1:def 7 :: thesis: for b₁, b₂ being Element of the carrier of (RRing A) holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (b₁ + b₂) * x = (b₁ * x) + (b₂ * x) )
thus for b₁, b₂ being Element of the carrier of (RRing A) holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (b₁ + b₂) * x = (b₁ * x) + (b₂ * x) ) by Th42; :: thesis: verum

end;

A7: RRing A is well-unital

proof

let x be Element of (RRing A); :: according to VECTSP_1:def 6 :: thesis: ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x )
thus ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x ) by Th42; :: thesis: verum

end;

A8: RRing A is associative

proof

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

end;

RRing A is commutative

proof

let x be Element of (RRing A); :: according to GROUP_1:def 12 :: thesis: for b₁ being Element of the carrier of (RRing A) holds x * b₁ = b₁ * x
thus for b₁ being Element of the carrier of (RRing A) holds x * b₁ = b₁ * x by Th42; :: thesis: verum

end;

hence RRing A is commutative Ring by A1, A2, A5, A3, A8, A7, A6; :: thesis: verum