let r be Real; :: thesis: for j being Element of NAT holds
( ( j <> 0 & r = 0 ) iff Product (j |-> r) = 0 )
let j be Element of NAT ; :: thesis: ( ( j <> 0 & r = 0 ) iff Product (j |-> r) = 0 )
set f = j |-> r;
A1: dom (j |-> r) = Seg j by FUNCOP_1:19;

hereby :: thesis: ( Product (j |-> r) = 0 implies ( j <> 0 & r = 0 ) )

assume that
A2: j <> 0 and
A3: r = 0 ; :: thesis: Product (j |-> r) = 0
consider n being Nat such that
A4: j = n + 1 by A2, NAT_1:6;
1 <= j by A4, NAT_1:11;
then A5: 1 in Seg j by FINSEQ_1:3;
then (j |-> r) . 1 = 0 by A3, FUNCOP_1:13;
hence Product (j |-> r) = 0 by A1, A5, RVSUM_1:133; :: thesis: verum

end;

assume Product (j |-> r) = 0 ; :: thesis: ( j <> 0 & r = 0 )
then ex n being Nat st
( n in dom (j |-> r) & (j |-> r) . n = 0 ) by RVSUM_1:133;
hence ( j <> 0 & r = 0 ) by A1, FUNCOP_1:13; :: thesis: verum