let n be non zero Nat; :: thesis: ( not addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is empty & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is Abelian & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is right_complementable & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is add-associative & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is right_zeroed )
A1: 1 <= n by NAT_1:14;
now :: thesis: INT.Ring n is Ringend;
then reconsider R = INT.Ring n as Ring ;
set S = addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #);
A2: for v, w being Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) holds v + w = w + v
proof
let v, w be Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #); :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of R ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum
end;
A3: for x being Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) holds x is right_complementable
proof
let v be Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #); :: thesis:
reconsider v1 = v as Element of R ;
consider w1 being Element of R such that
A4: v1 + w1 = 0. R by ALGSTR_0:def 11;
reconsider w = w1 as Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) ;
v + w = 0. addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) by A4;
hence v is right_complementable ; :: thesis: verum
end;
A5: for u, v, w being Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #); :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of R ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum
end;
A6: for v being Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) holds v + (0. addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #)) = v
proof
let v be Element of addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #); :: thesis: v + (0. addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #)) = v
reconsider v1 = v as Element of R ;
thus v + (0. addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #)) = v1 + (0. R)
.= v ; :: thesis: verum
end;
thus ( not addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is empty & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is Abelian & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is right_complementable & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is add-associative & addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) is right_zeroed ) by ; :: thesis: verum