let L be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p, s being Polynomial of L st s <> 0_. L holds
( s divides p iff ex t being Polynomial of L st t *' s = p )
let p, s be Polynomial of L; :: thesis: ( s <> 0_. L implies ( s divides p iff ex t being Polynomial of L st t *' s = p ) )
assume A1: s <> 0_. L ; :: thesis: ( s divides p iff ex t being Polynomial of L st t *' s = p )
A2: now :: thesis: ( ex t being Polynomial of L st t *' s = p implies s divides p )
(deg s) - 0 > 0 - 1 by A1, Lm8;
then A3: deg (0_. L) < deg s by Th20;
given t being Polynomial of L such that A4: t *' s = p ; :: thesis: s divides p
p = (t *' s) + (0_. L) by A4, POLYNOM3:28;
then p div s = t by A3, Def5;
then p mod s = 0_. L by A4, POLYNOM3:29;
hence s divides p ; :: thesis: verum
end;
now :: thesis: ( s divides p implies ex t being Polynomial of L st t *' s = p )
assume A5: s divides p ; :: thesis: ex t being Polynomial of L st t *' s = p
consider t being Polynomial of L such that
A6: p = ((p div s) *' s) + t and
deg t < deg s by A1, Def5;
p mod s = t + (((p div s) *' s) - ((p div s) *' s)) by A6, POLYNOM3:26
.= t + (0_. L) by POLYNOM3:29
.= t by POLYNOM3:28 ;
then t = 0_. L by A5;
then p = (p div s) *' s by A6, POLYNOM3:28;
hence ex t being Polynomial of L st t *' s = p ; :: thesis: verum
end;
hence ( s divides p iff ex t being Polynomial of L st t *' s = p ) by A2; :: thesis: verum