theorem :: MATRIXR2:39

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