i0 in NAT by ORDINAL1:def 13;
hence Swap (1. K,n),1,i0 is Matrix of n,K by AA330; :: thesis: verum