set k2 = n;
set ii = a,k1 <>0_goto n;
set J = Load (a,k1 <>0_goto n);

now

let n be Element of NAT ; :: thesis: for i being Instruction of st inspos n in dom (Load (a,k1 <>0_goto n)) & i = (Load (a,k1 <>0_goto n)) . (inspos n) holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of ; :: thesis: ( inspos n in dom (Load (a,k1 <>0_goto n)) & i = (Load (a,k1 <>0_goto n)) . (inspos n) implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A1: inspos n in dom (Load (a,k1 <>0_goto n)) and
A2: i = (Load (a,k1 <>0_goto n)) . (inspos n) ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
dom (Load (a,k1 <>0_goto n)) = {(inspos 0 )} by FUNCOP_1:19;
then inspos n = inspos 0 by A1, TARSKI:def 1;
then A3: a,k1 <>0_goto n = i by A2, FUNCOP_1:87;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:25; :: thesis: i valid_at n
A4: ( n + n >= 0 & InsCode i <> 6 ) by A3, SCMPDS_2:25;
( InsCode i <> 0 & InsCode i <> 5 ) by A3, SCMPDS_2:25;
hence i valid_at n by A3, A4, Def11; :: thesis: verum

end;

hence Load (a,k1 <>0_goto n) is shiftable by Def12; :: thesis: verum