A1: t is Element of INT * by FINSEQ_1:def 11;
ObjectKind f = INT * by SCMFSA_2:27;
hence f .--> t is FinPartState of by A1, AMI_1:59; :: thesis: verum