let F be FinSequence of REAL ; :: thesis:
assume A1: for i being Element of dom F holds
( 0 <= F . i & F . i <= 1 ) ; :: thesis:

per cases ;

suppose ex i being Nat st
( i in dom F & F . i = 0 ) ; :: thesis:

hence ( 0 <= Product F & Product F <= 1 ) by RVSUM_1:103; :: thesis:

end;

suppose A2: for i being Nat holds
( not i in dom F or not F . i = 0 ) ; :: thesis:

A3: for k being Element of NAT st k in dom F holds
F . k > 0

proof

let k be Element of NAT ; :: thesis:
assume A4: k in dom F ; :: thesis:
F . k <> 0 by A2, A4;
hence F . k > 0 by A1, A4; :: thesis:

end;

hence 0 <= Product F by NAT_4:42; :: thesis:
1 is Element of REAL by XREAL_0:def 1;
then reconsider G = (len F) |-> 1 as FinSequence of REAL by FINSEQ_2:63;
A6: len G = len F by CARD_1:def 7;
for k being Element of NAT st k in dom F holds
( F . k <= G . k & F . k > 0 )

proof

let k be Element of NAT ; :: thesis:
assume A7: k in dom F ; :: thesis:
A9: k in Seg (len F) by A7, FINSEQ_1:def 3;
F . k <= 1 by A1, A7;
hence F . k <= G . k by A9, FINSEQ_2:57; :: thesis:
thus F . k > 0 by A3, A7; :: thesis:

end;

then Product F <= Product G by A6, NAT_4:54;
hence Product F <= 1 by RVSUM_1:102; :: thesis:

end;

end;