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 S₁[ 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: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume AS: S₁[k] ; :: thesis: S₁[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 A1, POLYNOM5:19 ;
then consider r1 being Polynomial of R such that
A2: ((rpoly (1,a)) `^ k) *' r1 = p by AS, RING_4:1;
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 C, A2, RATFUNC1:5;
then b * r1 = (rpoly (1,a)) *' r by RATFUNC1:7;
then rpoly (1,a) divides r1 by divi1b, RING_4:1;
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 A2, A3, POLYNOM3:33
.= ((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 S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[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