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

per cases ( ex i being Nat st
( i in dom F & F . i = 0 ) or for i being Nat holds
( not i in dom F or not F . i = 0 ) ) ;

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

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

end;

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

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

proof

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

end;

hence 0 <= Product F by NAT_4:42; :: thesis: Product F <= 1
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: ( k in dom F implies ( F . k <= G . k & F . k > 0 ) )
assume A7: k in dom F ; :: thesis: ( F . k <= G . k & F . k > 0 )
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: F . k > 0
thus F . k > 0 by A3, A7; :: thesis: verum

end;

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

end;

end;