let R be Ring; :: thesis: for S being Subring of R
for a being Element of R
for b being Element of S st a = b holds
- a = - b
let S be Subring of R; :: thesis: for a being Element of R
for b being Element of S st a = b holds
- a = - b
let a be Element of R; :: thesis: for b being Element of S st a = b holds
- a = - b
let b be Element of S; :: thesis: ( a = b implies - a = - b )
assume AS: a = b ; :: thesis: - a = - b
the carrier of S c= the carrier of R by C0SP1:def 3;
then reconsider c = - b as Element of R ;
dom the addF of S = [: the carrier of S, the carrier of S:] by FUNCT_2:def 1;
then A6: [c,a] in dom the addF of S by AS, ZFMISC_1:def 2;
c + a = ( the addF of R || the carrier of S) . (c,a) by A6, FUNCT_1:49
.= (- b) + b by AS, C0SP1:def 3
.= 0. S by RLVECT_1:5
.= 0. R by C0SP1:def 3
.= (- a) + a by RLVECT_1:5 ;
hence - a = - b by RLVECT_1:8; :: thesis: verum