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