let F be INT -valued FinSequence of REAL ; :: thesis: ( len F is odd & ( for i being Nat st i in dom F holds
F . i is odd ) implies Sum F is odd )
assume A1: ( len F is odd & ( for i being Nat st i in dom F holds
F . i is odd ) ) ; :: thesis: Sum F is odd
A2: Sum F, Sum (F mod 2) are_congruent_mod 2 by NUMBER04:10;
F mod 2 = (len F) |-> 1

proof

C1: dom (F mod 2) = dom F by EULER_2:def 1
.= dom ((len F) |-> 1) by FINSEQ_1:def 3 ;
for i being Nat st i in dom (F mod 2) holds
(F mod 2) . i = ((len F) |-> 1) . i

proof

let i be Nat; :: thesis: ( i in dom (F mod 2) implies (F mod 2) . i = ((len F) |-> 1) . i )
assume i in dom (F mod 2) ; :: thesis: (F mod 2) . i = ((len F) |-> 1) . i
then D2: i in dom F by EULER_2:def 1;
then D3: F . i is odd by A1;
(F mod 2) . i = (F . i) mod 2 by D2, EULER_2:def 1
.= 1 by D3, NAT_2:22
.= ((dom F) --> 1) . i by D2, FUNCOP_1:7
.= ((len F) |-> 1) . i by FINSEQ_1:def 3 ;
hence (F mod 2) . i = ((len F) |-> 1) . i ; :: thesis: verum

end;

hence F mod 2 = (len F) |-> 1 by C1, FINSEQ_1:13; :: thesis: verum

end;

then Sum (F mod 2) = (len F) * 1 by RVSUM_1:80
.= len F ;
hence Sum F is odd by A2, A1; :: thesis: verum