Newbie question: SPARK verification condition on member of private record

[Tim Rowe <spamtrap@tgrowe.plus.net>]

Ok, I've been busily reading all of the spark documentation, and there's 
just one thing I'm stuck on at the moment.

I have:
    subtype Array_Index is Integer range 1..5000;
    type Foo is private;
    function Get_Order(This: in Foo) return Array_Index;
    -- other specifications

and in the private part I have
    type Foo is record
       Highest_Valid_Index: Array_Index;
       -- other definitions
    end record;

The body of Get_Order is simply
    function Get_Order(This: in Foo) return Array_Index is
    begin
       return This.Highest_Valid_Index;
    end Get_Order;

My problem is that I'm getting a proof obligation
H1:    get_order(this) < 5000 .
C1:    fld_highest_valid_index(this) <= 4999 .
If I'm reading that correctly then it's clearly true, but I would like 
to be able to annotate the code so that Examiner knows that 
get_order(this) = fld_highest_valid_index(this). My instinct is to 
annotate Get_Order with
    --# return This.Highest_Valid_Index;
but that's not allowed (" Semantic Error    :  9: Selected components 
are not allowed for This.")

So how should I annotate or restructure the code to make the 
relationship between Get_Order(This) and This.Highest_Valid_Index?

Thanks,

Tim Rowe