Insertion sort works like this : Start with one element compare with all elements we have and place it at correct position. The number to sort are known as key.

Input :

A sequence of numbers a₁, a₂, .., a_n

Output :

A permutation of input sequence such that a'₁ <= a'₂ ... <= a'_n

Insertion Sort (A):
    for j = 2 to A.length
    key = A[j]
    i = j - 1
    while i > 0 and A[i] > key
        A[i+1] = A[i]
        i = i -1
    A[i+1] = key

Loop Invariant is array A[1,...,j-1] which has element 1 to j-1 in sorted order . Loop invariant doesn't contribute to current sorting steps. Now for any algorithms to be loop invariant, it have to satisfy 3 properties:

1. Initialization : When j =2, subarray A[1,...,j-1] has only one element which is also first element of array A. So obviously, it is sorted array and holds property.
2. Maintenance : Now for each iteration, it is needed to show that the subarray if sorted before current iteration remains sorted in next iterations. In for looping, moving of A[j-1],A[j-2],A[j-3] and so on by one position right till loop finds proper position of A[j] is done and A[j] is then placed at that location. Thus subarray remains sorted even after end of iteration.
3. Termination : At the end of loop,  we can see array would remain sorted. Thus termination property holds.