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

now

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 Def5;
defpred S₁[ Nat] means for p being Polynomial of L st p = Sum (F | $1) holds
len p <= 1;
A3: S₁[ 0 ]

proof

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

end;

A5: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: for q being Polynomial of L st q = Sum (F | n) holds
len q <= 1 ; :: thesis: S₁[n + 1]
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
reconsider F1 = Sum (F | n) as Polynomial of L by POLYNOM3:def 12;
reconsider maxFq = max (len F1),(len ((p . n) * (<%x%> `^ n))) as Element of NAT by FINSEQ_2:1;
A8: len F1 <= 1 by A6;
len ((p . n) * (<%x%> `^ n)) <= 1

proof

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

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

then len ((p . n) * (<%x%> `^ n)) = len (<%x%> `^ n) by Th26
.= len <%((power L) . x,n)%> by Th37 ;
hence len ((p . n) * (<%x%> `^ n)) <= 1 by ALGSEQ_1:def 6; :: thesis: verum

end;

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

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

end;

end;

end;

then A9: maxFq <= 1 by A8, XXREAL_0:28;
A10: ( maxFq >= len F1 & maxFq >= len ((p . n) * (<%x%> `^ n)) ) by XXREAL_0:25;

now

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

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

n + 1 >= 1 by NAT_1:11;
then A12: n + 1 in dom F by A11, FINSEQ_3:27;
then A13: F /. (n + 1) = F . (n + 1) by PARTFUN1:def 8
.= (p . ((n + 1) -' 1)) * (<%x%> `^ ((n + 1) -' 1)) by A2, A12
.= (p . n) * (<%x%> `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . n) * (<%x%> `^ n) by NAT_D:34 ;
F | (n + 1) = (F | n) ^ <*(F /. (n + 1))*> by A11, JORDAN8:2;
then q = (Sum (F | n)) + (F /. (n + 1)) by A7, FVSUM_1:87
.= F1 + ((p . n) * (<%x%> `^ n)) by A13, POLYNOM3:def 12 ;
then len q <= maxFq by A10, POLYNOM4:9;
hence len q <= 1 by A9, XXREAL_0:2; :: thesis: verum

end;

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

then n >= len F by NAT_1:13;
then ( F | n = F & F | (n + 1) = F ) by A14, FINSEQ_1:79;
hence len q <= 1 by A6, A7; :: thesis: verum

end;

end;

end;

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

end;

A15: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A5);
F | (len F) = F by FINSEQ_1:79;
hence len (Subst p,<%x%>) <= 1 by A1, A15; :: thesis: verum

end;

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

end;

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