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 that
A1: p <> 0_. L and
A2: z is_a_root_of p ; :: thesis: deg (p div (rpoly 1,z)) = (deg p) - 1
consider s being Polynomial of L such that
A3: p = (rpoly 1,z) *' s by A2, Th33;
A4: rpoly 1,z <> 0_. L by A1, A3, POLYNOM4:5;
A5: 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 A3, 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;

s <> 0_. L by A1, A3, POLYNOM3:35;
then deg p = (deg (rpoly 1,z)) + (deg s) by A3, A4, Th23
.= 1 + (deg s) by Th27 ;
hence deg (p div (rpoly 1,z)) = (deg p) - 1 by A4, A5, Def5; :: thesis: verum