let n be Nat; :: thesis: (Seg n) --> the_set_of_all_open_real_bounded_intervals is n -element FinSequence
reconsider f = (Seg n) --> the_set_of_all_open_real_bounded_intervals as FinSequence ;
dom f is n -element by FUNCOP_1:13;
then card (dom f) = n by CARD_1:def 7;
then card f = n by CARD_1:62;
hence (Seg n) --> the_set_of_all_open_real_bounded_intervals is n -element FinSequence by CARD_1:def 7; :: thesis: verum