let R be Ring; for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
let S be RingExtension of R; for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
let p be Element of the carrier of (Polynom-Ring R); for q being Element of the carrier of (Polynom-Ring S) st p = q holds
for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
let q be Element of the carrier of (Polynom-Ring S); ( p = q implies for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q) )
assume AS1:
p = q
; for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
let T1 be RingExtension of S; for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
let T2 be RingExtension of R; ( T1 = T2 implies Roots (T2,p) = Roots (T1,q) )
assume AS2:
T1 = T2
; Roots (T2,p) = Roots (T1,q)
the carrier of (Polynom-Ring S) c= the carrier of (Polynom-Ring T1)
by FIELD_4:10;
then reconsider q1 = q as Element of the carrier of (Polynom-Ring T1) ;
the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring T2)
by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring T2) ;
thus Roots (T2,p) =
Roots p1
by FIELD_7:13
.=
Roots (T1,q)
by AS1, AS2, FIELD_7:13
; verum