let n be non zero Nat; :: thesis: ( not addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is empty & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is Abelian & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_complementable & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is add-associative & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_zeroed )

A1: 1 <= n by NAT_1:14;

then reconsider R = INT.Ring n as Ring ;

set S = addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #);

A2: for v, w being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds v + w = w + v

A1: 1 <= n by NAT_1:14;

then reconsider R = INT.Ring n as Ring ;

set S = addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #);

A2: for v, w being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds v + w = w + v

proof

A3:
for x being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds x is right_complementable
let v, w be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: 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;reconsider v1 = v, w1 = w as Element of R ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum

proof

A5:
for u, v, w being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds (u + v) + w = u + (v + w)
let v be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: thesis: v is right_complementable

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 (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) ;

v + w = 0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) by A4;

hence v is right_complementable ; :: thesis: verum

end;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 (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) ;

v + w = 0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) by A4;

hence v is right_complementable ; :: thesis: verum

proof

A6:
for v being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds v + (0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #)) = v
let u, v, w be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: 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;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

proof

thus
( not addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is empty & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is Abelian & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_complementable & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is add-associative & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_zeroed )
by A2, A3, A5, A6, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum
let v be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: thesis: v + (0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #)) = v

reconsider v1 = v as Element of R ;

thus v + (0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #)) = v1 + (0. R)

.= v ; :: thesis: verum

end;reconsider v1 = v as Element of R ;

thus v + (0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #)) = v1 + (0. R)

.= v ; :: thesis: verum