let L be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of L
for x being Element of L holds len (Subst (p,<%x%>)) <= 1
let p be Polynomial of L; :: thesis: for x being Element of L holds len (Subst (p,<%x%>)) <= 1
let x be Element of L; :: thesis: len (Subst (p,<%x%>)) <= 1

now :: thesis: len (Subst (p,<%x%>)) <= 1

now :: thesis: len (Subst (p,<%x%>)) <= 1

consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A1: Subst (p,<%x%>) = Sum F and
len F = len p and
A2: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (<%x%> `^ (n -' 1)) by Def6;
defpred S₁[ Nat] means for p being Polynomial of L st p = Sum (F | $1) holds
len p <= 1;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider F1 = Sum (F | n) as Polynomial of L by POLYNOM3:def 10;
reconsider maxFq = max ((len F1),(len ((p . nn) * (<%x%> `^ n)))) as Element of NAT by ORDINAL1:def 12;
A4: len ((p . nn) * (<%x%> `^ n)) <= 1

proof

per cases ( p . n <> 0. L or p . n = 0. L ) ;

suppose p . n <> 0. L ; :: thesis: len ((p . nn) * (<%x%> `^ n)) <= 1

then len ((p . nn) * (<%x%> `^ n)) = len (<%x%> `^ n) by Th25
.= len <%(power (x,n))%> by Th36 ;
hence len ((p . nn) * (<%x%> `^ n)) <= 1 by ALGSEQ_1:def 5; :: thesis: verum

end;

suppose p . n = 0. L ; :: thesis: len ((p . nn) * (<%x%> `^ n)) <= 1

hence len ((p . nn) * (<%x%> `^ n)) <= 1 by Th24; :: thesis: verum

end;

end;

end;

assume A5: for q being Polynomial of L st q = Sum (F | n) holds
len q <= 1 ; :: thesis: S₁[n + 1]
then len F1 <= 1 ;
then A6: maxFq <= 1 by A4, XXREAL_0:28;
let q be Polynomial of L; :: thesis: ( q = Sum (F | (n + 1)) implies len q <= 1 )
assume A7: q = Sum (F | (n + 1)) ; :: thesis: len q <= 1
A8: ( maxFq >= len F1 & maxFq >= len ((p . nn) * (<%x%> `^ n)) ) by XXREAL_0:25;

now :: thesis: len q <= 1

per cases ( n + 1 <= len F or n + 1 > len F ) ;

suppose A9: n + 1 <= len F ; :: thesis: len q <= 1

n + 1 >= 1 by NAT_1:11;
then A10: n + 1 in dom F by A9, FINSEQ_3:25;
then A11: F /. (n + 1) = F . (n + 1) by PARTFUN1:def 6
.= (p . ((n + 1) -' 1)) * (<%x%> `^ ((n + 1) -' 1)) by A2, A10
.= (p . nn) * (<%x%> `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (<%x%> `^ n) by NAT_D:34 ;
F | (n + 1) = (F | n) ^ <*(F /. (n + 1))*> by A9, FINSEQ_5:82;
then q = (Sum (F | n)) + (F /. (n + 1)) by A7, FVSUM_1:71
.= F1 + ((p . nn) * (<%x%> `^ n)) by A11, POLYNOM3:def 10 ;
then len q <= maxFq by A8, POLYNOM4:6;
hence len q <= 1 by A6, XXREAL_0:2; :: thesis: verum

end;

suppose A12: n + 1 > len F ; :: thesis: len q <= 1

then n >= len F by NAT_1:13;
then A13: F | n = F by FINSEQ_1:58;
F | (n + 1) = F by A12, FINSEQ_1:58;
hence len q <= 1 by A5, A7, A13; :: thesis: verum

end;

end;

end;

hence len q <= 1 ; :: thesis: verum

end;

A14: F | (len F) = F by FINSEQ_1:58;
A15: S₁[ 0 ]

proof

let p be Polynomial of L; :: thesis: ( p = Sum (F | 0) implies len p <= 1 )
A16: F | 0 = <*> the carrier of (Polynom-Ring L) ;
assume p = Sum (F | 0) ; :: thesis: len p <= 1
then p = 0. (Polynom-Ring L) by A16, RLVECT_1:43
.= 0_. L by POLYNOM3:def 10 ;
hence len p <= 1 by POLYNOM4:3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A3);
hence len (Subst (p,<%x%>)) <= 1 by A1, A14; :: thesis: verum

end;

hence len (Subst (p,<%x%>)) <= 1 ; :: thesis: verum

end;

hence len (Subst (p,<%x%>)) <= 1 ; :: thesis: verum