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)
proof
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;
A2: for a, b being Element of (INT.Ring 1) holds a + b = b + a
proof
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;
A3: for a being Element of (INT.Ring 1) holds a + (0. (INT.Ring 1)) = a
proof
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;
A4: for a, b, c being Element of (INT.Ring 1) holds (a * b) * c = a * (b * c)
proof
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;
A5: for a being Element of (INT.Ring 1) holds a + (- a) = 0. (INT.Ring 1)
proof
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;
A6: INT.Ring 1 is right_complementable
proof
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;
A7: for a, b, c being Element of (INT.Ring 1) holds (a + b) + c = a + (b + c)
proof
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;
A8: for a being Element of (INT.Ring 1) holds
( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a )
proof
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;
A10: INT.Ring 1 is well-unital by A8;
A11: for a, b being Element of (INT.Ring 1) holds a * b = b * a
proof
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;
A12: for a, b, c being Element of (INT.Ring 1) holds a * (b + c) = (a * b) + (a * c)
proof
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;
A13: for a, b, c being Element of (INT.Ring 1) holds (b + c) * a = (b * a) + (c * a)
proof
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;
0. (INT.Ring 1) = 0 by CARD_1:49, TARSKI:def 1
.= 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