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 () 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 () such that
A3: Sum F = f . (len F) and
A4: ( f . 0 = 0. () & ( for j being Nat
for v being Element of () 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: () . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
per cases ( n is odd or n is even ) ;
suppose A5: n is odd ; :: thesis: () . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
defpred S1[ Nat] means ( \$1 <= len F implies for P being Polynomial of L st P = f . \$1 holds
P . n = 0. L );
A6: S1[ 0 ]
proof
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 ;
hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum
end;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[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 ;
k + 1 in dom F by ;
then A12: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by ;
then reconsider Fk1 = F . (k + 1) as Element of () by POLYNOM3:def 10;
reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;
A13: P = (f . k) + Fk1 by
.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by ;
A14: fk . n = 0. L by ;
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 ;
hence P . n = 0. L ; :: thesis: verum
end;
for k being Nat holds S1[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 ; :: thesis: verum
end;
suppose A15: n is even ; :: thesis: () . 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;
per cases ( m < len F or m >= len F ) ;
suppose A17: m < len F ; :: thesis: () . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
defpred S1[ Nat] means ( \$1 <= len F implies for P being Polynomial of L st P = f . \$1 holds
P . n = p . n );
defpred S2[ Nat] means ( \$1 <= m implies for P being Polynomial of L st P = f . \$1 holds
P . n = 0. L );
A18: S2[ 0 ]
proof
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 ;
hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum
end;
A19: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A20: S2[k] ; :: thesis: S2[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 ;
A25: ( k < len F & k + 1 <= len F ) by ;
then k + 1 in dom F by ;
then A26: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by ;
then reconsider Fk1 = F . (k + 1) as Element of () 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 ;
A28: fk . n = 0. L by ;
n <> 2 * k by ;
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 ;
hence P . n = 0. L ; :: thesis: verum
end;
A29: for k being Nat holds S2[k] from A30: S1[m + 1]
proof
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 ;
A35: F . (m + 1) = ((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m) by ;
then reconsider Fm1 = F . (m + 1) as Element of () by POLYNOM3:def 10;
A36: P = (f . m) + Fm1 by
.= fm + (((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m)) by ;
A37: fm . n = 0. L by A29;
(<%(0. L),(0. L),(1_ L)%> `^ m) . n = 1_ L by ;
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 ;
hence P . n = p . n by ; :: thesis: verum
end;
A38: for k being Nat st m + 1 <= k & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( m + 1 <= k & S1[k] implies S1[k + 1] )
set k1 = k + 1;
assume A39: ( m + 1 <= k & S1[k] ) ; :: thesis: S1[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 ;
k + 1 in dom F by ;
then A43: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by ;
then reconsider Fk1 = F . (k + 1) as Element of () by POLYNOM3:def 10;
reconsider fk = f . k as Polynomial of L by POLYNOM3:def 10;
A44: P = (f . k) + Fk1 by
.= fk + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by ;
A45: fk . n = p . n by ;
n <> 2 * k by ;
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 ;
hence P . n = p . n ; :: thesis: verum
end;
A46: for k being Nat st m + 1 <= k holds
S1[k] from m + 1 <= len F by ;
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 ; :: thesis: verum
end;
suppose A47: m >= len F ; :: thesis: () . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
then A48: 2 * m >= 2 * (len (sieve (p,2))) by ;
A49: len () is_at_least_length_of even_part p by ALGSEQ_1:def 3;
2 * m >= len ()
proof
per cases ( len () = 0 or len () > 0 ) ;
suppose len () = 0 ; :: thesis: 2 * m >= len ()
hence 2 * m >= len () ; :: thesis: verum
end;
suppose len () > 0 ; :: thesis: 2 * m >= len ()
then 2 * (len (sieve (p,2))) = (len ()) + 1 by ;
hence 2 * m >= len () by ; :: thesis: verum
end;
end;
end;
then A50: (even_part p) . n = 0. L by ;
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
per cases ( len () = 0 or len () > 0 ) ;
suppose len () = 0 ; :: thesis: 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))
then len (sieve (p,2)) = 0 by ;
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;
suppose len () > 0 ; :: thesis: 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))
then 2 * (len (sieve (p,2))) = (len ()) + 1 by ;
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
.= ((len (sieve (p,2))) * 2) - 1 ;
then 2 * m >= (len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))) + 1 by ;
hence 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) by NAT_1:13; :: thesis: verum
end;
end;
end;
hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by ; :: thesis: verum
end;
end;
end;
end;