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