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
p <- (x -context_in 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
p <- (x -context_in 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
p <- (x -context_in 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
p <- (x -context_in 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
p <- (x -context_in p) = x -context_pos_in p
let p be Element of Args (o,(Free (S,X))); :: thesis: ( p is x -context_including implies p <- (x -context_in p) = x -context_pos_in p )
assume A1: p is x -context_including ; :: thesis: p <- (x -context_in p) = x -context_pos_in p
then p just_once_values x -context_in p by Th73;
then ( p <- (x -context_in p) in dom p & p . (p <- (x -context_in p)) = x -context_in p ) by FINSEQ_4:def 3;
hence p <- (x -context_in p) = x -context_pos_in p by A1, CPI; :: thesis: verum