let n be non zero Nat; :: thesis: (Seg n) --> REAL is non-empty n -element FinSequence
set X = (Seg n) --> REAL;
A1: ( dom ((Seg n) --> REAL) = Seg n & rng ((Seg n) --> REAL) = {REAL} ) by FUNCOP_1:8;
reconsider X = (Seg n) --> REAL as FinSequence ;
n is Element of NAT by ORDINAL1:def 12;
then len X = n by A1, FINSEQ_1:def 3;
hence (Seg n) --> REAL is non-empty n -element FinSequence by CARD_1:def 7; :: thesis: verum