let n be Nat; :: thesis: for R being domRing
for p being non zero Polynomial of R
for a being Element of R
for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

let R be domRing; :: thesis: for p being non zero Polynomial of R
for a being Element of R
for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

let p be non zero Polynomial of R; :: thesis: for a being Element of R
for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

let a be Element of R; :: thesis: for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

let b be non zero Element of R; :: thesis: ( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )
defpred S1[ Nat] means ( (rpoly (1,a)) `^ \$1 divides b * p implies (rpoly (1,a)) `^ \$1 divides p );
now :: thesis: ( (rpoly (1,a)) `^ 0 divides b * p implies (rpoly (1,a)) `^ 0 divides p )
assume (rpoly (1,a)) `^ 0 divides b * p ; :: thesis: (rpoly (1,a)) `^ 0 divides p
(rpoly (1,a)) `^ 0 = 1_. R by POLYNOM5:15;
then ((rpoly (1,a)) `^ 0) *' p = p ;
hence (rpoly (1,a)) `^ 0 divides p by RING_4:1; :: thesis: verum
end;
then IA: S1[ 0 ] ;
IS: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume AS: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( (rpoly (1,a)) `^ (k + 1) divides b * p implies (rpoly (1,a)) `^ (k + 1) divides p )
assume (rpoly (1,a)) `^ (k + 1) divides b * p ; :: thesis: (rpoly (1,a)) `^ (k + 1) divides p
then consider r being Polynomial of R such that
A1: ((rpoly (1,a)) `^ (k + 1)) *' r = b * p by RING_4:1;
C: ((rpoly (1,a)) `^ k) *' ((rpoly (1,a)) *' r) = (((rpoly (1,a)) `^ k) *' (rpoly (1,a))) *' r by POLYNOM3:33
.= b * p by ;
then consider r1 being Polynomial of R such that
A2: ((rpoly (1,a)) `^ k) *' r1 = p by ;
reconsider r1 = r1 as non zero Polynomial of R by A2;
(b * r1) *' ((rpoly (1,a)) `^ k) = ((rpoly (1,a)) *' r) *' ((rpoly (1,a)) `^ k) by ;
then b * r1 = (rpoly (1,a)) *' r by RATFUNC1:7;
then rpoly (1,a) divides r1 by ;
then consider r2 being Polynomial of R such that
A3: (rpoly (1,a)) *' r2 = r1 by RING_4:1;
p = (((rpoly (1,a)) `^ k) *' (rpoly (1,a))) *' r2 by
.= ((rpoly (1,a)) `^ (k + 1)) *' r2 by POLYNOM5:19 ;
hence (rpoly (1,a)) `^ (k + 1) divides p by RING_4:1; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(IA, IS);
hence ( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p ) by divi1; :: thesis: verum