let A, B be Ring; :: thesis: for x1 being Element of A st A is Subring of B holds
In ((- x1),B) = - (In (x1,B))
let x1 be Element of A; :: thesis: ( A is Subring of B implies In ((- x1),B) = - (In (x1,B)) )
assume A0: A is Subring of B ; :: thesis: In ((- x1),B) = - (In (x1,B))
(In ((- x1),B)) + (In (x1,B)) = In (((- x1) + x1),B) by A0, ALGNUM_1:8
.= In ((0. A),B) by RLVECT_1:5
.= 0. B by A0, Lm5 ;
hence In ((- x1),B) = - (In (x1,B)) by RLVECT_1:6; :: thesis: verum