let n be Nat; :: thesis: ( n > 0 implies ex f being positive-yielding FinSequence of NAT st
( len f = n & Sum f = Product f ) )
assume A1: n > 0 ; :: thesis: ex f being positive-yielding FinSequence of NAT st
( len f = n & Sum f = Product f )
( not not n = 0 & ... & not n = 2 or n > 2 ) ;

per cases then ( n = 1 or n >= 2 ) by A1;

suppose A2: n = 1 ; :: thesis: ex f being positive-yielding FinSequence of NAT st
( len f = n & Sum f = Product f )

set f = <* the positive Nat*>;
reconsider f = <* the positive Nat*> as positive-yielding FinSequence of NAT by FINSEQ_1:103;
take f ; :: thesis: ( len f = n & Sum f = Product f )
thus len f = n by A2, FINSEQ_1:39; :: thesis: Sum f = Product f
thus Sum f = Product f ; :: thesis: verum

end;

suppose n >= 2 ; :: thesis: ex f being positive-yielding FinSequence of NAT st
( len f = n & Sum f = Product f )

then reconsider n2 = n - 2 as Element of NAT by INT_1:5;
set g = n2 |-> 1;
set f = (n2 |-> 1) ^ <*2,n*>;
reconsider f = (n2 |-> 1) ^ <*2,n*> as positive-yielding FinSequence of NAT by A1, FINSEQ_1:102;
take f ; :: thesis: ( len f = n & Sum f = Product f )
len <*2,n*> = 2 by FINSEQ_1:44;
hence n = (len (n2 |-> 1)) + (len <*2,n*>)
.= len f by FINSEQ_1:22 ;
:: thesis: Sum f = Product f
A3: Product <*2,n*> = 2 * n by RVSUM_1:99;
A4: Product (n2 |-> 1) = 1 by RVSUM_1:102;
A5: Sum <*2,n*> = 2 + n by RVSUM_1:77;
A6: Sum (n2 |-> 1) = (n - 2) * 1 by RVSUM_1:80;
thus Sum f = (Sum (n2 |-> 1)) + (Sum <*2,n*>) by RVSUM_1:75
.= (Product (n2 |-> 1)) * (Product <*2,n*>) by A3, A4, A5, A6
.= Product f by RVSUM_1:97 ; :: thesis: verum

end;

end;