for f being Permutation of (Seg 0) holds f = <*> NAT ;