let f be constant non empty real-valued FinSequence; :: thesis: Product f = (the_value_of f) |^ (len f)
set r = the_value_of f;
set i = len f;
f = (dom f) --> (the_value_of f) by FUNCOP_1:80
.= (len f) |-> (the_value_of f) by FINSEQ_1:def 3 ;
hence Product f = (the_value_of f) |^ (len f) by NEWTON:def 1; :: thesis: verum