let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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

assume A3: s divides p ; :: thesis: ex t being Polynomial of L st t *' s = p
consider t being Polynomial of L such that
A4: ( p = ((p div s) *' s) + t & deg t < deg s ) by A1, Def5;
p mod s = t + (((p div s) *' s) - ((p div s) *' s)) by A4, POLYNOM3:26
.= t + (0_. L) by POLYNOM3:30
.= t by POLYNOM3:29 ;
then t = 0_. L by A3, Def7;
then p = (p div s) *' s by A4, POLYNOM3:29;
hence ex t being Polynomial of L st t *' s = p ; :: thesis: verum

end;

now

given t being Polynomial of L such that A5: t *' s = p ; :: thesis: s divides p
A6: p = (t *' s) + (0_. L) by A5, POLYNOM3:29;
(deg s) - 0 > 0 - 1 by A1, Lm9;
then deg (0_. L) < deg s by Th20;
then p div s = t by A6, Def5;
then p mod s = 0_. L by A5, POLYNOM3:30;
hence s divides p by Def7; :: thesis: verum

end;

hence ( s divides p iff ex t being Polynomial of L st t *' s = p ) by A2; :: thesis: verum