let R be Ring; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
let T2 be RingExtension of R; :: thesis: ( T1 = T2 implies Roots (T2,p) = Roots (T1,q) )
assume AS2: T1 = T2 ; :: thesis: 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 ; :: thesis: verum