reconsider i = i as Element of NAT by ORDINAL1:def 13;
i .--> I is NAT -defined FinPartState of ;
hence i .--> I is NAT -defined FinPartState of ; :: thesis: verum