let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for z0 being Element of L holds - <%z0%> = <%(- z0)%>
let z0 be Element of L; :: thesis: - <%z0%> = <%(- z0)%>
set p = <%z0%>;
set r = <%(- z0)%>;
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (- <%z0%>) . n = <%(- z0)%> . n
A1: dom (- <%z0%>) = NAT by FUNCT_2:def 1;
A2: (- <%z0%>) . n = (- <%z0%>) /. n
.= - (<%z0%> /. n) by A1, VFUNCT_1:def 5
.= - (<%z0%> . n) ;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: (- <%z0%>) . n = <%(- z0)%> . n

then ( <%z0%> . n = z0 & <%(- z0)%> . n = - z0 ) by POLYNOM5:32;
hence (- <%z0%>) . n = <%(- z0)%> . n by A2; :: thesis: verum

end;

suppose n > 0 ; :: thesis: (- <%z0%>) . n = <%(- z0)%> . n

then n >= 0 + 1 by NAT_1:13;
then ( <%z0%> . n = 0. L & <%(- z0)%> . n = 0. L ) by POLYNOM5:32;
hence (- <%z0%>) . n = <%(- z0)%> . n by A2; :: thesis: verum

end;

end;