let L be Field; :: thesis: for p being Polynomial of L holds even_part p = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)

let p be Polynomial of L; :: thesis: even_part p = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)

set C = sieve (p,2);

set x2 = <%(0. L),(0. L),(1_ L)%>;

set Cx = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>);

set E = even_part p;

consider F being FinSequence of (Polynom-Ring L) such that

A1: ( Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) = Sum F & len F = len (sieve (p,2)) ) and

A2: for n being Element of NAT st n in dom F holds

F . n = ((sieve (p,2)) . (n -' 1)) * (<%(0. L),(0. L),(1_ L)%> `^ (n -' 1)) by POLYNOM5:def 6;

consider f being sequence of (Polynom-Ring L) such that

A3: Sum F = f . (len F) and

A4: ( f . 0 = 0. (Polynom-Ring L) & ( for j being Nat

for v being Element of (Polynom-Ring L) st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 12;

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n

let p be Polynomial of L; :: thesis: even_part p = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)

set C = sieve (p,2);

set x2 = <%(0. L),(0. L),(1_ L)%>;

set Cx = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>);

set E = even_part p;

consider F being FinSequence of (Polynom-Ring L) such that

A1: ( Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) = Sum F & len F = len (sieve (p,2)) ) and

A2: for n being Element of NAT st n in dom F holds

F . n = ((sieve (p,2)) . (n -' 1)) * (<%(0. L),(0. L),(1_ L)%> `^ (n -' 1)) by POLYNOM5:def 6;

consider f being sequence of (Polynom-Ring L) such that

A3: Sum F = f . (len F) and

A4: ( f . 0 = 0. (Polynom-Ring L) & ( for j being Nat

for v being Element of (Polynom-Ring L) st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 12;

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n

per cases
( n is odd or n is even )
;

end;

suppose A5:
n is odd
; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n

defpred S_{1}[ Nat] means ( $1 <= len F implies for P being Polynomial of L st P = f . $1 holds

P . n = 0. L );

A6: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A6, A7);

then (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n = 0. L by A1, A3;

hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by A5, HURWITZ2:def 1; :: thesis: verum

end;P . n = 0. L );

A6: S

proof

A7:
for k being Nat st S
assume
0 <= len F
; :: thesis: for P being Polynomial of L st P = f . 0 holds

P . n = 0. L

let P be Polynomial of L; :: thesis: ( P = f . 0 implies P . n = 0. L )

assume P = f . 0 ; :: thesis: P . n = 0. L

then P = 0_. L by A4, POLYNOM3:def 10;

hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum

end;P . n = 0. L

let P be Polynomial of L; :: thesis: ( P = f . 0 implies P . n = 0. L )

assume P = f . 0 ; :: thesis: P . n = 0. L

then P = 0_. L by A4, POLYNOM3:def 10;

hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A8: S_{1}[k]
; :: thesis: S_{1}[k + 1]

set k1 = k + 1;

assume A9: k + 1 <= len F ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds

P . n = 0. L

let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = 0. L )

assume A10: P = f . (k + 1) ; :: thesis: P . n = 0. L

A11: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;

k + 1 in dom F by A9, NAT_1:11, FINSEQ_3:25;

then A12: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A11, A2;

then reconsider Fk1 = F . (k + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;

A13: P = (f . k) + Fk1 by A10, A9, NAT_1:13, A4

.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by A12, POLYNOM3:def 10 ;

A14: fk . n = 0. L by A9, NAT_1:13, A8;

n <> 2 * k by A5;

then (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;

then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4

.= 0. L ;

then P . n = (0. L) + (0. L) by A13, A14, NORMSP_1:def 2;

hence P . n = 0. L ; :: thesis: verum

end;assume A8: S

set k1 = k + 1;

assume A9: k + 1 <= len F ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds

P . n = 0. L

let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = 0. L )

assume A10: P = f . (k + 1) ; :: thesis: P . n = 0. L

A11: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;

k + 1 in dom F by A9, NAT_1:11, FINSEQ_3:25;

then A12: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A11, A2;

then reconsider Fk1 = F . (k + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;

A13: P = (f . k) + Fk1 by A10, A9, NAT_1:13, A4

.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by A12, POLYNOM3:def 10 ;

A14: fk . n = 0. L by A9, NAT_1:13, A8;

n <> 2 * k by A5;

then (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;

then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4

.= 0. L ;

then P . n = (0. L) + (0. L) by A13, A14, NORMSP_1:def 2;

hence P . n = 0. L ; :: thesis: verum

then (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n = 0. L by A1, A3;

hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by A5, HURWITZ2:def 1; :: thesis: verum

suppose A15:
n is even
; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n

then consider m being Nat such that

A16: 2 * m = n by ABIAN:def 2;

set m1 = m + 1;

end;A16: 2 * m = n by ABIAN:def 2;

set m1 = m + 1;

per cases
( m < len F or m >= len F )
;

end;

suppose A17:
m < len F
; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n

defpred S_{1}[ Nat] means ( $1 <= len F implies for P being Polynomial of L st P = f . $1 holds

P . n = p . n );

defpred S_{2}[ Nat] means ( $1 <= m implies for P being Polynomial of L st P = f . $1 holds

P . n = 0. L );

A18: S_{2}[ 0 ]
_{2}[k] holds

S_{2}[k + 1]
_{2}[k]
from NAT_1:sch 2(A18, A19);

A30: S_{1}[m + 1]
_{1}[k] holds

S_{1}[k + 1]

S_{1}[k]
from NAT_1:sch 8(A30, A38);

m + 1 <= len F by A17, NAT_1:13;

then (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n = p . n by A1, A3, A46;

hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by A15, HURWITZ2:def 1; :: thesis: verum

end;P . n = p . n );

defpred S

P . n = 0. L );

A18: S

proof

A19:
for k being Nat st S
assume
0 <= m
; :: thesis: for P being Polynomial of L st P = f . 0 holds

P . n = 0. L

let P be Polynomial of L; :: thesis: ( P = f . 0 implies P . n = 0. L )

assume P = f . 0 ; :: thesis: P . n = 0. L

then P = 0_. L by A4, POLYNOM3:def 10;

hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum

end;P . n = 0. L

let P be Polynomial of L; :: thesis: ( P = f . 0 implies P . n = 0. L )

assume P = f . 0 ; :: thesis: P . n = 0. L

then P = 0_. L by A4, POLYNOM3:def 10;

hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum

S

proof

A29:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A20: S_{2}[k]
; :: thesis: S_{2}[k + 1]

set k1 = k + 1;

assume A21: k + 1 <= m ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds

P . n = 0. L

then A22: k < m by NAT_1:13;

let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = 0. L )

assume A23: P = f . (k + 1) ; :: thesis: P . n = 0. L

A24: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;

A25: ( k < len F & k + 1 <= len F ) by A22, A17, A21, XXREAL_0:2;

then k + 1 in dom F by NAT_1:11, FINSEQ_3:25;

then A26: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A24, A2;

then reconsider Fk1 = F . (k + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;

A27: P = (f . k) + Fk1 by A23, A4, A25

.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by A26, POLYNOM3:def 10 ;

A28: fk . n = 0. L by NAT_1:13, A20, A21;

n <> 2 * k by A16, A21, NAT_1:13;

then (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;

then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4

.= 0. L ;

then P . n = (0. L) + (0. L) by A27, A28, NORMSP_1:def 2;

hence P . n = 0. L ; :: thesis: verum

end;assume A20: S

set k1 = k + 1;

assume A21: k + 1 <= m ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds

P . n = 0. L

then A22: k < m by NAT_1:13;

let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = 0. L )

assume A23: P = f . (k + 1) ; :: thesis: P . n = 0. L

A24: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;

A25: ( k < len F & k + 1 <= len F ) by A22, A17, A21, XXREAL_0:2;

then k + 1 in dom F by NAT_1:11, FINSEQ_3:25;

then A26: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A24, A2;

then reconsider Fk1 = F . (k + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;

A27: P = (f . k) + Fk1 by A23, A4, A25

.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by A26, POLYNOM3:def 10 ;

A28: fk . n = 0. L by NAT_1:13, A20, A21;

n <> 2 * k by A16, A21, NAT_1:13;

then (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;

then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4

.= 0. L ;

then P . n = (0. L) + (0. L) by A27, A28, NORMSP_1:def 2;

hence P . n = 0. L ; :: thesis: verum

A30: S

proof

A38:
for k being Nat st m + 1 <= k & S
assume A31:
m + 1 <= len F
; :: thesis: for P being Polynomial of L st P = f . (m + 1) holds

P . n = p . n

let P be Polynomial of L; :: thesis: ( P = f . (m + 1) implies P . n = p . n )

assume A32: P = f . (m + 1) ; :: thesis: P . n = p . n

reconsider fm = f . m as Polynomial of L by POLYNOM3:def 10;

A33: 1 <= m + 1 by NAT_1:11;

A34: (m + 1) -' 1 = (m + 1) - 1 by NAT_1:11, XREAL_1:233;

A35: F . (m + 1) = ((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m) by A34, A2, A33, A31, FINSEQ_3:25;

then reconsider Fm1 = F . (m + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

A36: P = (f . m) + Fm1 by A32, A31, NAT_1:13, A4

.= fm + (((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m)) by A35, POLYNOM3:def 10 ;

A37: fm . n = 0. L by A29;

(<%(0. L),(0. L),(1_ L)%> `^ m) . n = 1_ L by A16, Th10;

then (((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m)) . n = ((sieve (p,2)) . m) * (1_ L) by POLYNOM5:def 4

.= (sieve (p,2)) . m ;

then P . n = (0. L) + ((sieve (p,2)) . m) by A36, A37, NORMSP_1:def 2;

hence P . n = p . n by Def5, A16; :: thesis: verum

end;P . n = p . n

let P be Polynomial of L; :: thesis: ( P = f . (m + 1) implies P . n = p . n )

assume A32: P = f . (m + 1) ; :: thesis: P . n = p . n

reconsider fm = f . m as Polynomial of L by POLYNOM3:def 10;

A33: 1 <= m + 1 by NAT_1:11;

A34: (m + 1) -' 1 = (m + 1) - 1 by NAT_1:11, XREAL_1:233;

A35: F . (m + 1) = ((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m) by A34, A2, A33, A31, FINSEQ_3:25;

then reconsider Fm1 = F . (m + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

A36: P = (f . m) + Fm1 by A32, A31, NAT_1:13, A4

.= fm + (((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m)) by A35, POLYNOM3:def 10 ;

A37: fm . n = 0. L by A29;

(<%(0. L),(0. L),(1_ L)%> `^ m) . n = 1_ L by A16, Th10;

then (((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m)) . n = ((sieve (p,2)) . m) * (1_ L) by POLYNOM5:def 4

.= (sieve (p,2)) . m ;

then P . n = (0. L) + ((sieve (p,2)) . m) by A36, A37, NORMSP_1:def 2;

hence P . n = p . n by Def5, A16; :: thesis: verum

S

proof

A46:
for k being Nat st m + 1 <= k holds
let k be Nat; :: thesis: ( m + 1 <= k & S_{1}[k] implies S_{1}[k + 1] )

set k1 = k + 1;

assume A39: ( m + 1 <= k & S_{1}[k] )
; :: thesis: S_{1}[k + 1]

assume A40: k + 1 <= len F ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds

P . n = p . n

let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = p . n )

assume A41: P = f . (k + 1) ; :: thesis: P . n = p . n

A42: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;

k + 1 in dom F by A40, NAT_1:11, FINSEQ_3:25;

then A43: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A42, A2;

then reconsider Fk1 = F . (k + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;

A44: P = (f . k) + Fk1 by A41, A4, A40, NAT_1:13

.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by A43, POLYNOM3:def 10 ;

A45: fk . n = p . n by A40, NAT_1:13, A39;

n <> 2 * k by A16, A39, NAT_1:13;

then (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;

then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4

.= 0. L ;

then P . n = (p . n) + (0. L) by A44, A45, NORMSP_1:def 2;

hence P . n = p . n ; :: thesis: verum

end;set k1 = k + 1;

assume A39: ( m + 1 <= k & S

assume A40: k + 1 <= len F ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds

P . n = p . n

let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = p . n )

assume A41: P = f . (k + 1) ; :: thesis: P . n = p . n

A42: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;

k + 1 in dom F by A40, NAT_1:11, FINSEQ_3:25;

then A43: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A42, A2;

then reconsider Fk1 = F . (k + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;

A44: P = (f . k) + Fk1 by A41, A4, A40, NAT_1:13

.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by A43, POLYNOM3:def 10 ;

A45: fk . n = p . n by A40, NAT_1:13, A39;

n <> 2 * k by A16, A39, NAT_1:13;

then (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;

then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4

.= 0. L ;

then P . n = (p . n) + (0. L) by A44, A45, NORMSP_1:def 2;

hence P . n = p . n ; :: thesis: verum

S

m + 1 <= len F by A17, NAT_1:13;

then (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n = p . n by A1, A3, A46;

hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by A15, HURWITZ2:def 1; :: thesis: verum

suppose A47:
m >= len F
; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n

then A48:
2 * m >= 2 * (len (sieve (p,2)))
by A1, XREAL_1:64;

A49: len (even_part p) is_at_least_length_of even_part p by ALGSEQ_1:def 3;

2 * m >= len (even_part p)

A51: len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) is_at_least_length_of Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) by ALGSEQ_1:def 3;

D: 2 = 2 * 1 ;

2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))

end;A49: len (even_part p) is_at_least_length_of even_part p by ALGSEQ_1:def 3;

2 * m >= len (even_part p)

proof
end;

then A50:
(even_part p) . n = 0. L
by A16, ALGSEQ_1:def 2, A49;A51: len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) is_at_least_length_of Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) by ALGSEQ_1:def 3;

D: 2 = 2 * 1 ;

2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))

proof
end;

hence
(even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
by A16, A50, ALGSEQ_1:def 2, A51; :: thesis: verumper cases
( len (even_part p) = 0 or len (even_part p) > 0 )
;

end;

suppose
len (even_part p) = 0
; :: thesis: 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))

then
len (sieve (p,2)) = 0
by D, Th21;

then sieve (p,2) = 0_. L by POLYNOM4:5;

then Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) = 0_. L by POLYNOM5:49;

hence 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) by POLYNOM4:3; :: thesis: verum

end;then sieve (p,2) = 0_. L by POLYNOM4:5;

then Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) = 0_. L by POLYNOM5:49;

hence 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) by POLYNOM4:3; :: thesis: verum

suppose
len (even_part p) > 0
; :: thesis: 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))

then
2 * (len (sieve (p,2))) = (len (even_part p)) + 1
by Th18, Th20;

then A52: len (sieve (p,2)) <> 0 ;

len <%(0. L),(0. L),(1_ L)%> = 3 by NIVEN:28;

then len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) = ((((len (sieve (p,2))) * 3) - (len (sieve (p,2)))) - 3) + 2 by A52, POLYNOM5:52

.= ((len (sieve (p,2))) * 2) - 1 ;

then 2 * m >= (len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))) + 1 by A47, A1, XREAL_1:64;

hence 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) by NAT_1:13; :: thesis: verum

end;then A52: len (sieve (p,2)) <> 0 ;

len <%(0. L),(0. L),(1_ L)%> = 3 by NIVEN:28;

then len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) = ((((len (sieve (p,2))) * 3) - (len (sieve (p,2)))) - 3) + 2 by A52, POLYNOM5:52

.= ((len (sieve (p,2))) * 2) - 1 ;

then 2 * m >= (len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))) + 1 by A47, A1, XREAL_1:64;

hence 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) by NAT_1:13; :: thesis: verum