let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )
let s be SortSymbol of S; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )
let x be Element of X . s; :: thesis: for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )
let p be Element of Args (o,(Free (S,X))); :: thesis: ( p is x -context_including implies ( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) ) )
assume A0: p is x -context_including ; :: thesis: ( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )
then A1: p . (x -context_pos_in p) is context of x by CPI;
thus x -context_pos_in p in dom p by A0, CPI; :: thesis: x -context_in p = p . (x -context_pos_in p)
then p . (x -context_pos_in p) in rng p by FUNCT_1:def 3;
hence x -context_in p = p . (x -context_pos_in p) by A0, A1, CIn; :: thesis: verum