let i be Nat; :: thesis: for S being non empty non void ManySortedSign
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 & x -context_pos_in p <> i & i in dom p holds
p /. i is x -omitting
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 & x -context_pos_in p <> i & i in dom p holds
p /. i is x -omitting
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 & x -context_pos_in p <> i & i in dom p holds
p /. i is x -omitting
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 & x -context_pos_in p <> i & i in dom p holds
p /. i is x -omitting
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 & x -context_pos_in p <> i & i in dom p holds
p /. i is x -omitting
let x be Element of X . s; :: thesis: for p being Element of Args (o,(Free (S,X))) st p is x -context_including & x -context_pos_in p <> i & i in dom p holds
p /. i is x -omitting
let p be Element of Args (o,(Free (S,X))); :: thesis: ( p is x -context_including & x -context_pos_in p <> i & i in dom p implies p /. i is x -omitting )
assume A1: ( p is x -context_including & x -context_pos_in p <> i & i in dom p ) ; :: thesis: p /. i is x -omitting
then consider j being Nat such that
A2: ( j in dom p & p . j is context of x & ( for n being Nat
for t being Element of (Free (S,X)) st n in dom p & n <> j & t = p . n holds
t is x -omitting ) ) ;
A3: x -context_pos_in p = j by A1, A2, CPI;
p /. i = p . i by A1, PARTFUN1:def 6;
hence p /. i is x -omitting by A1, A2, A3; :: thesis: verum