let f, g be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( (len (~ f)) * (len (~ g)) <> 0 implies len (~ (f * g)) = ((len (~ f)) + (len (~ g))) - 1 )
reconsider p = ~ f, q = ~ g as Polynomial of INT.Ring ;
assume (len (~ f)) * (len (~ g)) <> 0 ; :: thesis: len (~ (f * g)) = ((len (~ f)) + (len (~ g))) - 1
then A2: ( len p > 0 & len q > 0 ) ;
( p . ((len p) -' 1) <> 0. INT.Ring & q . ((len q) -' 1) <> 0. INT.Ring ) by A2, UPROOTS:18;
then (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. INT.Ring ;
then len (p *' q) = ((len p) + (len q)) - 1 by POLYNOM4:10;
hence len (~ (f * g)) = ((len (~ f)) + (len (~ g))) - 1 by POLYNOM3:def 10; :: thesis: verum