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