RK is Element of Funcs ((Seg k),(n -tuples_on BOOLEAN)) by FINSEQ_2:93;
hence RK . i is Element of n -tuples_on BOOLEAN by FUNCT_2:5; :: thesis: verum