let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L
for z being Element of L st p <> 0_. L & z is_a_root_of p holds
deg (p div (rpoly 1,z)) = (deg p) - 1
let p be Polynomial of L; :: thesis: for z being Element of L st p <> 0_. L & z is_a_root_of p holds
deg (p div (rpoly 1,z)) = (deg p) - 1
let z be Element of L; :: thesis: ( p <> 0_. L & z is_a_root_of p implies deg (p div (rpoly 1,z)) = (deg p) - 1 )
assume A1: ( p <> 0_. L & z is_a_root_of p ) ; :: thesis: deg (p div (rpoly 1,z)) = (deg p) - 1
then consider s being Polynomial of L such that
A2: p = (rpoly 1,z) *' s by Th33;
A3: s <> 0_. L by A1, A2, POLYNOM3:35;
A4: rpoly 1,z <> 0_. L by A1, A2, POLYNOM4:5;
then A5: deg p = (deg (rpoly 1,z)) + (deg s) by A2, A3, Th23
.= 1 + (deg s) by Th27 ;
ex t being Polynomial of L st
( p = (s *' (rpoly 1,z)) + t & deg t < deg (rpoly 1,z) )

proof

take t = 0_. L; :: thesis: ( p = (s *' (rpoly 1,z)) + t & deg t < deg (rpoly 1,z) )
thus (s *' (rpoly 1,z)) + t = p by A2, POLYNOM3:29; :: thesis: deg t < deg (rpoly 1,z)
deg t = - 1 by Th20;
hence deg t < deg (rpoly 1,z) by Th27; :: thesis: verum

end;

hence deg (p div (rpoly 1,z)) = (deg p) - 1 by A4, A5, Def5; :: thesis: verum