let R be Ring; :: thesis: for R being Subring of R
for x being Element of R
for x1 being Element of R st x = x1 holds
- x = - x1
let S be Subring of R; :: thesis: for x being Element of R
for x1 being Element of S st x = x1 holds
- x = - x1
let x be Element of R; :: thesis: for x1 being Element of S st x = x1 holds
- x = - x1
let x1 be Element of S; :: thesis: ( x = x1 implies - x = - x1 )
set C = the carrier of R;
set C1 = the carrier of S;
set a = - x1;
assume A1: x = x1 ; :: thesis: - x = - x1
the carrier of S c= the carrier of R by C0SP1:def 3;
then reconsider g = - x1 as Element of R ;
x + g = x1 + (- x1) by A1, Th17
.= 0. S by VECTSP_1:19
.= 0. R by C0SP1:def 3 ;
hence - x = - x1 by VECTSP_1:16; :: thesis: verum