let i1, i2 be Nat; :: thesis: ( p . i1 is context of x & p . i2 is context of x implies i1 = i2 )
assume that
A1: p . i1 is context of x and
A2: p . i2 is context of x ; :: thesis: i1 = i2
reconsider C1 = p . i1, C2 = p . i2 as context of x by A1, A2;
( i1 in dom p & i2 in dom p ) by A1, A2, FUNCT_1:def 2;
then ( ( i1 <> i implies C1 is x -omitting ) & ( i2 <> i implies C2 is x -omitting ) ) by B;
hence i1 = i2 ; :: thesis: verum