let R be domRing; :: thesis: for S being domRingExtension of R
for a being Element of R
for b being Element of S holds
( not b ^2 = a ^2 or b = a or b = - a )
let S be domRingExtension of R; :: thesis: for a being Element of R
for b being Element of S holds
( not b ^2 = a ^2 or b = a or b = - a )
let a be Element of R; :: thesis: for b being Element of S holds
( not b ^2 = a ^2 or b = a or b = - a )
let b be Element of S; :: thesis: ( not b ^2 = a ^2 or b = a or b = - a )
assume AS: b ^2 = a ^2 ; :: thesis: ( b = a or b = - a )
A: R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
then reconsider a1 = a as Element of S ;
a1 ^2 = a1 * a1 by O_RING_1:def 1
.= a * a by A, FIELD_6:16
.= b ^2 by AS, O_RING_1:def 1 ;
then ( b = a1 or b = - a1 ) by REALALG2:10;
hence ( b = a or b = - a ) by A, FIELD_6:17; :: thesis: verum