let L be Ring; :: thesis: for a being Element of L holds
( deg (a | L) = 0 iff a <> 0. L )
let a be Element of L; :: thesis: ( deg (a | L) = 0 iff a <> 0. L )

now :: thesis: ( a <> 0. L implies deg (a | L) = 0 )

assume Y: a <> 0. L ; :: thesis: deg (a | L) = 0

now :: thesis: not deg (a | L) < 0

assume deg (a | L) < 0 ; :: thesis: contradiction
then a | L = 0_. L by T8b
.= (0. L) | L by T6 ;
hence contradiction by Y, T9; :: thesis: verum

end;

hence deg (a | L) = 0 by RATFUNC1:def 2; :: thesis: verum

end;

hence ( deg (a | L) = 0 iff a <> 0. L ) by T8b, T6; :: thesis: verum