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

per cases then ( n = 0 or n = 1 or n = 2 or n > 2 ) ;

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

then ( <%z0,z1,z2%> . n = z0 & <%(- z0),(- z1),(- z2)%> . n = - z0 ) by Th21;
hence (- <%z0,z1,z2%>) . n = <%(- z0),(- z1),(- z2)%> . n by A2; :: thesis: verum

end;

suppose n = 1 ; :: thesis: (- <%z0,z1,z2%>) . n = <%(- z0),(- z1),(- z2)%> . n

then ( <%z0,z1,z2%> . n = z1 & <%(- z0),(- z1),(- z2)%> . n = - z1 ) by Th22;
hence (- <%z0,z1,z2%>) . n = <%(- z0),(- z1),(- z2)%> . n by A2; :: thesis: verum

end;

suppose n = 2 ; :: thesis: (- <%z0,z1,z2%>) . n = <%(- z0),(- z1),(- z2)%> . n

then ( <%z0,z1,z2%> . n = z2 & <%(- z0),(- z1),(- z2)%> . n = - z2 ) by Th23;
hence (- <%z0,z1,z2%>) . n = <%(- z0),(- z1),(- z2)%> . n by A2; :: thesis: verum

end;

suppose n > 2 ; :: thesis: (- <%z0,z1,z2%>) . n = <%(- z0),(- z1),(- z2)%> . n

then n >= 2 + 1 by NAT_1:13;
then ( <%z0,z1,z2%> . n = 0. L & <%(- z0),(- z1),(- z2)%> . n = 0. L ) by Th24;
hence (- <%z0,z1,z2%>) . n = <%(- z0),(- z1),(- z2)%> . n by A2; :: thesis: verum

end;

end;