let R be Ring; :: thesis: for S being RingExtension of R
for a being Element of R
for b being Element of S st a = b holds
- a = - b
let S be RingExtension 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 A1: a = b ; :: thesis: - a = - b
A2: R is Subring of S by Def1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
then reconsider x = - a as Element of S ;
A3: [a,(- a)] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
A4: the addF of S || the carrier of R = the addF of R by A2, C0SP1:def 3;
b + x = a + (- a) by A1, A4, A3, FUNCT_1:49
.= 0. R by RLVECT_1:5
.= 0. S by A2, C0SP1:def 3 ;
hence - a = - b by RLVECT_1:def 10; :: thesis: verum