let rr be Real; :: thesis: for j being Nat holds
( ( j <> 0 & rr = 0 ) iff Product (j |-> rr) = 0 )
let j be Nat; :: thesis: ( ( j <> 0 & rr = 0 ) iff Product (j |-> rr) = 0 )
set f = j |-> rr;
A1: dom (j |-> rr) = Seg j by FUNCOP_1:13;
hereby :: thesis: ( Product (j |-> rr) = 0 implies ( j <> 0 & rr = 0 ) )
assume that
A2: j <> 0 and
A3: rr = 0 ; :: thesis: Product (j |-> rr) = 0
ex n being Nat st j = n + 1 by A2, NAT_1:6;
then 1 <= j by NAT_1:11;
then A4: 1 in Seg j by FINSEQ_1:1;
then (j |-> rr) . 1 = 0 by A3, FUNCOP_1:7;
hence Product (j |-> rr) = 0 by A1, A4, RVSUM_1:103; :: thesis: verum
end;
assume Product (j |-> rr) = 0 ; :: thesis: ( j <> 0 & rr = 0 )
then ex n being Nat st
( n in dom (j |-> rr) & (j |-> rr) . n = 0 ) by RVSUM_1:103;
hence ( j <> 0 & rr = 0 ) by A1, FUNCOP_1:7; :: thesis: verum