let n be Nat; :: thesis: product ((Seg n) --> REAL) = REAL n
REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
hence product ((Seg n) --> REAL) = REAL n by CARD_3:11; :: thesis: verum