let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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:2;
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:28; :: 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:34;
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