set n = 1;

set R = INT.Ring 1;

A1: for x being Element of (INT.Ring 1) st x <> 0. (INT.Ring 1) holds

ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1)

( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a )

A11: for a, b being Element of (INT.Ring 1) holds a * b = b * a

.= 1. (INT.Ring 1) by CARD_1:49, TARSKI:def 1 ;

hence ( INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is almost_left_invertible & INT.Ring 1 is unital & INT.Ring 1 is distributive & INT.Ring 1 is commutative ) by A1, A2, A11, A7, A4, A3, A13, A12, A6, A10, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 7; :: thesis: verum

set R = INT.Ring 1;

A1: for x being Element of (INT.Ring 1) st x <> 0. (INT.Ring 1) holds

ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1)

proof

A2:
for a, b being Element of (INT.Ring 1) holds a + b = b + a
let x be Element of (INT.Ring 1); :: thesis: ( x <> 0. (INT.Ring 1) implies ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1) )

assume x <> 0. (INT.Ring 1) ; :: thesis: ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1)

then x <> 0 by SUBSET_1:def 8;

hence ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1) by CARD_1:49, TARSKI:def 1; :: thesis: verum

end;assume x <> 0. (INT.Ring 1) ; :: thesis: ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1)

then x <> 0 by SUBSET_1:def 8;

hence ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1) by CARD_1:49, TARSKI:def 1; :: thesis: verum

proof

A3:
for a being Element of (INT.Ring 1) holds a + (0. (INT.Ring 1)) = a
let a, b be Element of (INT.Ring 1); :: thesis: a + b = b + a

thus a + b = 0 by CARD_1:49, TARSKI:def 1

.= b + a by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

end;thus a + b = 0 by CARD_1:49, TARSKI:def 1

.= b + a by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

proof

A4:
for a, b, c being Element of (INT.Ring 1) holds (a * b) * c = a * (b * c)
let a be Element of (INT.Ring 1); :: thesis: a + (0. (INT.Ring 1)) = a

a = 0 by CARD_1:49, TARSKI:def 1;

hence a + (0. (INT.Ring 1)) = a by CARD_1:49, TARSKI:def 1; :: thesis: verum

end;a = 0 by CARD_1:49, TARSKI:def 1;

hence a + (0. (INT.Ring 1)) = a by CARD_1:49, TARSKI:def 1; :: thesis: verum

proof

A5:
for a being Element of (INT.Ring 1) holds a + (- a) = 0. (INT.Ring 1)
let a, b, c be Element of (INT.Ring 1); :: thesis: (a * b) * c = a * (b * c)

thus (a * b) * c = 0 by CARD_1:49, TARSKI:def 1

.= a * (b * c) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

end;thus (a * b) * c = 0 by CARD_1:49, TARSKI:def 1

.= a * (b * c) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

proof

A6:
INT.Ring 1 is right_complementable
let a be Element of (INT.Ring 1); :: thesis: a + (- a) = 0. (INT.Ring 1)

thus a + (- a) = 0 by CARD_1:49, TARSKI:def 1

.= 0. (INT.Ring 1) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

end;thus a + (- a) = 0 by CARD_1:49, TARSKI:def 1

.= 0. (INT.Ring 1) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

proof

A7:
for a, b, c being Element of (INT.Ring 1) holds (a + b) + c = a + (b + c)
let v be Element of (INT.Ring 1); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

take - v ; :: according to ALGSTR_0:def 11 :: thesis: v + (- v) = 0. (INT.Ring 1)

thus v + (- v) = 0. (INT.Ring 1) by A5; :: thesis: verum

end;take - v ; :: according to ALGSTR_0:def 11 :: thesis: v + (- v) = 0. (INT.Ring 1)

thus v + (- v) = 0. (INT.Ring 1) by A5; :: thesis: verum

proof

A8:
for a being Element of (INT.Ring 1) holds
let a, b, c be Element of (INT.Ring 1); :: thesis: (a + b) + c = a + (b + c)

thus (a + b) + c = 0 by CARD_1:49, TARSKI:def 1

.= a + (b + c) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

end;thus (a + b) + c = 0 by CARD_1:49, TARSKI:def 1

.= a + (b + c) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a )

proof

A10:
INT.Ring 1 is well-unital
by A8;
let a be Element of (INT.Ring 1); :: thesis: ( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a )

A9: a * (1. (INT.Ring 1)) = 0 by CARD_1:49, TARSKI:def 1

.= a by CARD_1:49, TARSKI:def 1 ;

(1. (INT.Ring 1)) * a = 0 by CARD_1:49, TARSKI:def 1

.= a by CARD_1:49, TARSKI:def 1 ;

hence ( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a ) by A9; :: thesis: verum

end;A9: a * (1. (INT.Ring 1)) = 0 by CARD_1:49, TARSKI:def 1

.= a by CARD_1:49, TARSKI:def 1 ;

(1. (INT.Ring 1)) * a = 0 by CARD_1:49, TARSKI:def 1

.= a by CARD_1:49, TARSKI:def 1 ;

hence ( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a ) by A9; :: thesis: verum

A11: for a, b being Element of (INT.Ring 1) holds a * b = b * a

proof

A12:
for a, b, c being Element of (INT.Ring 1) holds a * (b + c) = (a * b) + (a * c)
let a, b be Element of (INT.Ring 1); :: thesis: a * b = b * a

thus a * b = 0 by CARD_1:49, TARSKI:def 1

.= b * a by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

end;thus a * b = 0 by CARD_1:49, TARSKI:def 1

.= b * a by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

proof

A13:
for a, b, c being Element of (INT.Ring 1) holds (b + c) * a = (b * a) + (c * a)
let a, b, c be Element of (INT.Ring 1); :: thesis: a * (b + c) = (a * b) + (a * c)

thus a * (b + c) = 0 by CARD_1:49, TARSKI:def 1

.= (a * b) + (a * c) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

end;thus a * (b + c) = 0 by CARD_1:49, TARSKI:def 1

.= (a * b) + (a * c) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

proof

0. (INT.Ring 1) =
0
by CARD_1:49, TARSKI:def 1
let a, b, c be Element of (INT.Ring 1); :: thesis: (b + c) * a = (b * a) + (c * a)

thus (b + c) * a = 0 by CARD_1:49, TARSKI:def 1

.= (b * a) + (c * a) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

end;thus (b + c) * a = 0 by CARD_1:49, TARSKI:def 1

.= (b * a) + (c * a) by CARD_1:49, TARSKI:def 1 ; :: thesis: verum

.= 1. (INT.Ring 1) by CARD_1:49, TARSKI:def 1 ;

hence ( INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is almost_left_invertible & INT.Ring 1 is unital & INT.Ring 1 is distributive & INT.Ring 1 is commutative ) by A1, A2, A11, A7, A4, A3, A13, A12, A6, A10, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 7; :: thesis: verum