let n be Nat; :: thesis: 0* n in BOOLEAN *
n |-> FALSE is FinSequence of BOOLEAN ;
hence 0* n in BOOLEAN * by FINSEQ_1:def 11; :: thesis: verum