let t1, t2 be context of x; ( t1 in rng p & t2 in rng p implies t1 = t2 )
assume that
A3:
t1 in rng p
and
A4:
t2 in rng p
; t1 = t2
consider i1 being object such that
A5:
( i1 in dom p & t1 = p . i1 )
by A3, FUNCT_1:def 3;
consider i2 being object such that
A6:
( i2 in dom p & t2 = p . i2 )
by A4, FUNCT_1:def 3;
reconsider i1 = i1, i2 = i2 as Nat by A5, A6;
A7:
( i1 <> i implies t1 is x -omitting )
by B, A5;
( i2 <> i implies t2 is x -omitting )
by B, A6;
hence
t1 = t2
by A5, A6, A7; verum