let p be Element of (Formal-Series L); :: according to ALGSTR_0:def 16 :: thesis: p is right_complementable

reconsider p1 = p as sequence of L by Def2;

reconsider q = - p1 as Element of (Formal-Series L) by Def2;

take q ; :: according to ALGSTR_0:def 11 :: thesis: p + q = 0. (Formal-Series L)

thus p + q = p1 + (- p1) by Def2

.= p1 - p1 by POLYNOM3:def 6

.= 0_. L by POLYNOM3:29

.= 0. (Formal-Series L) by Def2 ; :: thesis: verum

reconsider p1 = p as sequence of L by Def2;

reconsider q = - p1 as Element of (Formal-Series L) by Def2;

take q ; :: according to ALGSTR_0:def 11 :: thesis: p + q = 0. (Formal-Series L)

thus p + q = p1 + (- p1) by Def2

.= p1 - p1 by POLYNOM3:def 6

.= 0_. L by POLYNOM3:29

.= 0. (Formal-Series L) by Def2 ; :: thesis: verum