InsCode (SubFrom a,k1,b,k2) = 10 by SCMPDS_2:31;
hence SubFrom a,k1,b,k2 is shiftable by Def13; :: thesis: verum