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

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