let L be Field; :: thesis: for p, q being Polynomial of L st len p <> 0 & len q > 1 holds
len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
let p, q be Polynomial of L; :: thesis: ( len p <> 0 & len q > 1 implies len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2 )
assume that
A1: len p <> 0 and
A2: len q > 1 ; :: thesis: len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A3: Subst (p,q) = Sum F and
A4: len F = len p and
A5: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) by Def6;
A6: 0 + 1 <= len F by A1, A4, NAT_1:13;
then A7: 1 in dom F by FINSEQ_3:25;
reconsider k = ((((len p) * (len q)) - (len p)) - (len q)) + 1 as Element of NAT by A1, A2, Th1, INT_1:3;
len p >= 0 + 1 by A1, NAT_1:13;
then A8: (len p) - 1 >= 0 ;
A9: len (q `^ ((len F) -' 1)) = ((((len p) -' 1) * (len q)) - ((len p) -' 1)) + 1 by A2, A4, Th23
.= ((((len p) -' 1) * (len q)) - ((len p) - 1)) + 1 by A8, XREAL_0:def 2
.= ((((len p) - 1) * (len q)) - ((len p) - 1)) + 1 by A8, XREAL_0:def 2
.= ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1) ;
A10: len (Subst (p,q)) >= ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1)

proof

set lF1 = (len F) -' 1;
set F1 = F | ((len F) -' 1);
reconsider sF1 = Sum (F | ((len F) -' 1)) as Polynomial of L by POLYNOM3:def 10;
A11: len F = ((len F) -' 1) + 1 by A6, XREAL_1:235;
then A12: F = (F | ((len F) -' 1)) ^ <*(F /. (len F))*> by FINSEQ_5:21;
then A13: Sum F = (Sum (F | ((len F) -' 1))) + (F /. (len F)) by FVSUM_1:71;
A14: len F = (len (F | ((len F) -' 1))) + 1 by A12, FINSEQ_2:16;
assume A15: len (Subst (p,q)) < ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1) ; :: thesis: contradiction
then len (Subst (p,q)) < k + 1 ;
then len (Subst (p,q)) <= k by NAT_1:13;
then A16: (Subst (p,q)) . k = 0. L by ALGSEQ_1:8;

now :: thesis: contradiction

per cases ( len (F | ((len F) -' 1)) <> {} or len (F | ((len F) -' 1)) = {} ) ;

suppose A17: len (F | ((len F) -' 1)) <> {} ; :: thesis: contradiction

defpred S₁[ Nat] means for F2 being Polynomial of L st F2 = Sum ((F | ((len F) -' 1)) | $1) holds
len F2 <= ((($1 * (len q)) - (len q)) - $1) + 2;
A18: (F | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = F | ((len F) -' 1) by FINSEQ_1:58;
A19: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A20: for F2 being Polynomial of L st F2 = Sum ((F | ((len F) -' 1)) | n) holds
len F2 <= (((n * (len q)) - (len q)) - n) + 2 ; :: thesis: S₁[n + 1]
len q >= 0 + (1 + 1) by A2, NAT_1:13;
then (len q) - 2 >= 0 by XREAL_1:19;
then (((n * (len q)) - n) + 1) + 0 <= (((n * (len q)) - n) + 1) + ((len q) - 2) by XREAL_1:7;
then ( ((((n * (len q)) - (len q)) - n) + 2) + 0 <= ((((n * (len q)) - (len q)) - n) + 2) + 1 & (((n * (len q)) - n) + 1) - ((len q) - 2) <= ((n * (len q)) - n) + 1 ) by XREAL_1:6, XREAL_1:20;
then A21: (((n * (len q)) - (len q)) - n) + 2 <= ((n * (len q)) - n) + 1 by XXREAL_0:2;
reconsider F3 = Sum ((F | ((len F) -' 1)) | n) as Polynomial of L by POLYNOM3:def 10;
let F2 be Polynomial of L; :: thesis: ( F2 = Sum ((F | ((len F) -' 1)) | (n + 1)) implies len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 )
assume A22: F2 = Sum ((F | ((len F) -' 1)) | (n + 1)) ; :: thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
len F3 <= (((n * (len q)) - (len q)) - n) + 2 by A20;
then A23: len F3 <= ((n * (len q)) - n) + 1 by A21, XXREAL_0:2;

now :: thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2

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

suppose A24: n + 1 <= len (F | ((len F) -' 1)) ; :: thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2

reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A25: n + 1 >= 1 by NAT_1:11;
reconsider maxFq = max ((len F3),(len ((p . nn) * (q `^ nn)))) as Element of NAT by ORDINAL1:def 12;
A26: ( maxFq >= len F3 & maxFq >= len ((p . nn) * (q `^ nn)) ) by XXREAL_0:25;
len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1

proof

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

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

then len ((p . nn) * (q `^ nn)) = len (q `^ nn) by Th25;
hence len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1 by A2, Th23; :: thesis: verum

end;

suppose A27: p . n = 0. L ; :: thesis: len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1

len q >= 0 + 1 by A2;
then (len q) - 1 >= 0 ;
then A28: n * ((len q) - 1) >= 0 ;
n * (len q) <= (n * (len q)) + 1 by NAT_1:11;
then (n * (len q)) - n <= ((n * (len q)) + 1) - n by XREAL_1:9;
hence len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1 by A27, A28, Th24; :: thesis: verum

end;

end;

end;

then A29: maxFq <= ((n * (len q)) - n) + 1 by A23, XXREAL_0:28;
len (F | ((len F) -' 1)) <= len F by A14, NAT_1:11;
then n + 1 <= len F by A24, XXREAL_0:2;
then A30: n + 1 in dom F by A25, FINSEQ_3:25;
A31: n + 1 in dom (F | ((len F) -' 1)) by A24, A25, FINSEQ_3:25;
then A32: (F | ((len F) -' 1)) /. (n + 1) = (F | ((len F) -' 1)) . (n + 1) by PARTFUN1:def 6
.= F . (n + 1) by A12, A31, FINSEQ_1:def 7
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A5, A30
.= (p . nn) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (q `^ nn) by NAT_D:34 ;
(F | ((len F) -' 1)) | (nn + 1) = ((F | ((len F) -' 1)) | nn) ^ <*((F | ((len F) -' 1)) /. (nn + 1))*> by A24, FINSEQ_5:82;
then F2 = (Sum ((F | ((len F) -' 1)) | n)) + ((F | ((len F) -' 1)) /. (n + 1)) by A22, FVSUM_1:71
.= F3 + ((p . nn) * (q `^ nn)) by A32, POLYNOM3:def 10 ;
then len F2 <= maxFq by A26, POLYNOM4:6;
hence len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by A29, XXREAL_0:2; :: thesis: verum

end;

suppose A33: n + 1 > len (F | ((len F) -' 1)) ; :: thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2

- (len q) <= - 1 by A2, XREAL_1:24;
then ((n * (len q)) - n) + (- (len q)) <= ((n * (len q)) - n) + (- 1) by XREAL_1:6;
then A34: (((n * (len q)) - (len q)) - n) + 2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by XREAL_1:6;
n >= len (F | ((len F) -' 1)) by A33, NAT_1:13;
then A35: (F | ((len F) -' 1)) | n = F | ((len F) -' 1) by FINSEQ_1:58;
(F | ((len F) -' 1)) | (n + 1) = F | ((len F) -' 1) by A33, FINSEQ_1:58;
then len F2 <= (((n * (len q)) - (len q)) - n) + 2 by A20, A22, A35;
hence len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by A34, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 ; :: thesis: verum

end;

0 + (len q) >= 1 + 1 by A2, NAT_1:13;
then 2 - (len q) <= 0 by XREAL_1:20;
then A36: (2 - (len q)) + k <= 0 + k by XREAL_1:6;
0 + 1 <= len (F | ((len F) -' 1)) by A17, NAT_1:13;
then A37: 1 in dom (F | ((len F) -' 1)) by FINSEQ_3:25;
A38: S₁[1]

proof

let F2 be Polynomial of L; :: thesis: ( F2 = Sum ((F | ((len F) -' 1)) | 1) implies len F2 <= (((1 * (len q)) - (len q)) - 1) + 2 )
Z: (F | ((len F) -' 1)) . 1 = (F | ((len F) -' 1)) /. 1 by A37, PARTFUN1:def 6;
(F | ((len F) -' 1)) | 1 = <*((F | ((len F) -' 1)) . 1)*> by A17, CARD_1:27, FINSEQ_5:20;
then A39: Sum ((F | ((len F) -' 1)) | 1) = (F | ((len F) -' 1)) . 1 by Z, RLVECT_1:44
.= F . 1 by A12, A37, FINSEQ_1:def 7
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0) * (q `^ (1 -' 1)) by XREAL_1:232
.= (p . 0) * (q `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
assume F2 = Sum ((F | ((len F) -' 1)) | 1) ; :: thesis: len F2 <= (((1 * (len q)) - (len q)) - 1) + 2
hence len F2 <= (((1 * (len q)) - (len q)) - 1) + 2 by A39, ALGSEQ_1:def 5; :: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A38, A19);
then len sF1 <= ((((len (F | ((len F) -' 1))) * (len q)) - (len q)) - (len (F | ((len F) -' 1)))) + 2 by A17, A18;
then A40: sF1 . k = 0. L by A4, A14, A36, ALGSEQ_1:8, XXREAL_0:2;
A41: len F in dom F by A6, FINSEQ_3:25;
then F /. (len F) = F . (len F) by PARTFUN1:def 6
.= (p . ((len F) -' 1)) * (q `^ ((len F) -' 1)) by A5, A41 ;
then Subst (p,q) = sF1 + ((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) by A3, A13, POLYNOM3:def 10;
then A42: (Subst (p,q)) . k = (sF1 . k) + (((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k) by NORMSP_1:def 2
.= ((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k by A40, RLVECT_1:def 4
.= (p . ((len F) -' 1)) * ((q `^ ((len F) -' 1)) . k) by Def4 ;
len (q `^ ((len F) -' 1)) = k + 1 by A9;
then A43: (q `^ ((len F) -' 1)) . k <> 0. L by ALGSEQ_1:10;
p . ((len F) -' 1) <> 0. L by A4, A11, ALGSEQ_1:10;
hence contradiction by A16, A42, A43, VECTSP_1:12; :: thesis: verum

end;

suppose A44: len (F | ((len F) -' 1)) = {} ; :: thesis: contradiction

A45: F /. 1 = F . 1 by A7, PARTFUN1:def 6
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0) * (q `^ (1 -' 1)) by XREAL_1:232
.= (p . 0) * (q `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
A46: 0. (Polynom-Ring L) = 0_. L by POLYNOM3:def 10;
A47: len F = 0 + 1 by A12, A44, FINSEQ_2:16;
then A48: p . 0 <> 0. L by A4, ALGSEQ_1:10;
F | ((len F) -' 1) = <*> the carrier of (Polynom-Ring L) by A44;
then Sum F = (0. (Polynom-Ring L)) + (F /. 1) by A13, A47, RLVECT_1:43
.= (0_. L) + <%(p . 0)%> by A45, A46, POLYNOM3:def 10
.= <%(p . 0)%> by POLYNOM3:28 ;
hence contradiction by A3, A4, A15, A47, A48, Th33; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

defpred S₁[ Nat] means for F1 being Polynomial of L st F1 = Sum (F | $1) holds
len F1 <= len (q `^ ($1 -' 1));
A49: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A50: for F1 being Polynomial of L st F1 = Sum (F | n) holds
len F1 <= len (q `^ (n -' 1)) ; :: thesis: S<sub>1</sub>[n + 1]
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider F2 = Sum (F | n) as Polynomial of L by POLYNOM3:def 10;
let F1 be Polynomial of L; :: thesis: ( F1 = Sum (F | (n + 1)) implies len F1 <= len (q `^ ((n + 1) -' 1)) )
assume A51: F1 = Sum (F | (n + 1)) ; :: thesis: len F1 <= len (q `^ ((n + 1) -' 1))
(n * (len q)) + ((len q) -' 1) >= n * (len q) by NAT_1:11;
then A52: (n * (len q)) - ((len q) -' 1) <= n * (len q) by XREAL_1:20;
len q >= 0 + 1 by A2;
then (len q) - 1 >= 0 ;
then (n * (len q)) - ((len q) - 1) <= n * (len q) by A52, XREAL_0:def 2;
then (((n * (len q)) - (len q)) + 1) - n <= (n * (len q)) - n by XREAL_1:9;
then A53: ((((n * (len q)) - (len q)) - n) + 1) + 1 <= ((n * (len q)) - n) + 1 by XREAL_1:6;
len (q `^ (n -' 1)) = (((n -' 1) * (len q)) - (n -' 1)) + 1 by A2, Th23
.= (((n - 1) * (len q)) - (n -' 1)) + 1 by XREAL_0:def 2
.= (((n * (len q)) - (1 * (len q))) - (n - 1)) + 1 by XREAL_0:def 2
.= ((((n * (len q)) - (len q)) - n) + 1) + 1 ;
then A54: len (q `^ (n -' 1)) <= len (q `^ nn) by A2, A53, Th23;

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

suppose A55: n + 1 <= len F ; :: thesis: len F1 <= len (q `^ ((n + 1) -' 1))

reconsider maxFq = max ((len F2),(len ((p . nn) * (q `^ nn)))) as Element of NAT by ORDINAL1:def 12;
( p . n <> 0. L or p . n = 0. L ) ;
then A56: len ((p . nn) * (q `^ nn)) <= len (q `^ nn) by Th24, Th25;
len F2 <= len (q `^ (n -' 1)) by A50;
then len F2 <= len (q `^ nn) by A54, XXREAL_0:2;
then A57: maxFq <= len (q `^ nn) by A56, XXREAL_0:28;
F | (n + 1) = (F | n) ^ <*(F /. (nn + 1))*> by A55, FINSEQ_5:82;
then A58: F1 = (Sum (F | n)) + (F /. (n + 1)) by A51, FVSUM_1:71;
n + 1 >= 1 by NAT_1:11;
then A59: n + 1 in dom F by A55, FINSEQ_3:25;
then F /. (n + 1) = F . (n + 1) by PARTFUN1:def 6
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A5, A59
.= (p . nn) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (q `^ nn) by NAT_D:34 ;
then A60: F1 = F2 + ((p . nn) * (q `^ nn)) by A58, POLYNOM3:def 10;
( maxFq >= len F2 & maxFq >= len ((p . nn) * (q `^ nn)) ) by XXREAL_0:25;
then len F1 <= maxFq by A60, POLYNOM4:6;
then len F1 <= len (q `^ nn) by A57, XXREAL_0:2;
hence len F1 <= len (q `^ ((n + 1) -' 1)) by NAT_D:34; :: thesis: verum

end;

suppose A61: n + 1 > len F ; :: thesis: len F1 <= len (q `^ ((n + 1) -' 1))

then n >= len F by NAT_1:13;
then A62: F | n = F by FINSEQ_1:58;
F | (n + 1) = F by A61, FINSEQ_1:58;
then len F1 <= len (q `^ (n -' 1)) by A50, A51, A62;
then len F1 <= len (q `^ nn) by A54, XXREAL_0:2;
hence len F1 <= len (q `^ ((n + 1) -' 1)) by NAT_D:34; :: thesis: verum

end;

end;

end;

A63: F | (len F) = F by FINSEQ_1:58;
A64: S₁[1]

proof

let F1 be Polynomial of L; :: thesis: ( F1 = Sum (F | 1) implies len F1 <= len (q `^ (1 -' 1)) )
Z: F . 1 = F /. 1 by A7, PARTFUN1:def 6;
F | 1 = <*(F . 1)*> by A1, A4, CARD_1:27, FINSEQ_5:20;
then A65: Sum (F | 1) = F . 1 by Z, RLVECT_1:44
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0) * (q `^ (1 -' 1)) by XREAL_1:232
.= (p . 0) * (q `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
assume F1 = Sum (F | 1) ; :: thesis: len F1 <= len (q `^ (1 -' 1))
then len F1 <= 1 by A65, ALGSEQ_1:def 5;
then len F1 <= len (1_. L) by POLYNOM4:4;
then len F1 <= len (q `^ 0) by Th15;
hence len F1 <= len (q `^ (1 -' 1)) by XREAL_1:232; :: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A64, A49);
then len (Subst (p,q)) <= len (q `^ ((len F) -' 1)) by A1, A3, A4, A63;
hence len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2 by A9, A10, XXREAL_0:1; :: thesis: verum