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