let a, b be Element of (Polynom-Ring L); :: according to INT_3:def 9 :: thesis: ( b = 0. (Polynom-Ring L) or ex b₁, b₂ being Element of the carrier of (Polynom-Ring L) st
( a = (b₁ * b) + b₂ & ( b₂ = 0. (Polynom-Ring L) or not (deg* L) . b <= (deg* L) . b₂ ) ) )
assume b <> 0. (Polynom-Ring L) ; :: thesis: ex b₁, b₂ being Element of the carrier of (Polynom-Ring L) st
( a = (b₁ * b) + b₂ & ( b₂ = 0. (Polynom-Ring L) or not (deg* L) . b <= (deg* L) . b₂ ) )
then not b is zero ;
hence ex b₁, b₂ being Element of the carrier of (Polynom-Ring L) st
( a = (b₁ * b) + b₂ & ( b₂ = 0. (Polynom-Ring L) or not (deg* L) . b <= (deg* L) . b₂ ) ) by thEucl1; :: thesis: verum