let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for z0, z1 being Element of L holds - <%z0,z1%> = <%(- z0),(- z1)%>
let z0, z1 be Element of L; :: thesis: - <%z0,z1%> = <%(- z0),(- z1)%>
set p = <%z0,z1%>;
set r = <%(- z0),(- z1)%>;
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (- <%z0,z1%>) . n = <%(- z0),(- z1)%> . n
A1: dom (- <%z0,z1%>) = NAT by FUNCT_2:def 1;
A2: (- <%z0,z1%>) . n = (- <%z0,z1%>) /. n
.= - (<%z0,z1%> /. n) by A1, VFUNCT_1:def 5
.= - (<%z0,z1%> . n) ;
( not not n = 0 & ... & not n = 1 or n > 1 ) ;
per cases then ( n = 0 or n = 1 or n > 1 ) ;
suppose n = 0 ; :: thesis: (- <%z0,z1%>) . n = <%(- z0),(- z1)%> . n
then ( <%z0,z1%> . n = z0 & <%(- z0),(- z1)%> . n = - z0 ) by POLYNOM5:38;
hence (- <%z0,z1%>) . n = <%(- z0),(- z1)%> . n by A2; :: thesis: verum
end;
suppose n = 1 ; :: thesis: (- <%z0,z1%>) . n = <%(- z0),(- z1)%> . n
then ( <%z0,z1%> . n = z1 & <%(- z0),(- z1)%> . n = - z1 ) by POLYNOM5:38;
hence (- <%z0,z1%>) . n = <%(- z0),(- z1)%> . n by A2; :: thesis: verum
end;
suppose n > 1 ; :: thesis: (- <%z0,z1%>) . n = <%(- z0),(- z1)%> . n
then n >= 1 + 1 by NAT_1:13;
then ( <%z0,z1%> . n = 0. L & <%(- z0),(- z1)%> . n = 0. L ) by POLYNOM5:38;
hence (- <%z0,z1%>) . n = <%(- z0),(- z1)%> . n by A2; :: thesis: verum
end;
end;