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
the_sort_of (x -context_in p) = (the_arity_of o) . (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
the_sort_of (x -context_in p) = (the_arity_of o) . (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
the_sort_of (x -context_in p) = (the_arity_of o) . (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
the_sort_of (x -context_in p) = (the_arity_of o) . (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
the_sort_of (x -context_in p) = (the_arity_of o) . (x -context_pos_in p)
let p be Element of Args (o,(Free (S,X))); :: thesis: ( p is x -context_including implies the_sort_of (x -context_in p) = (the_arity_of o) . (x -context_pos_in p) )
assume p is x -context_including ; :: thesis: the_sort_of (x -context_in p) = (the_arity_of o) . (x -context_pos_in p)
then ( x -context_pos_in p in dom p & dom p = dom (the_arity_of o) & x -context_in p = p . (x -context_pos_in p) ) by Th71, MSUALG_3:6;
then ( (the_arity_of o) /. (x -context_pos_in p) = (the_arity_of o) . (x -context_pos_in p) & x -context_in p in the Sorts of (Free (S,X)) . ((the_arity_of o) /. (x -context_pos_in p)) ) by PARTFUN1:def 6, MSUALG_6:2;
hence the_sort_of (x -context_in p) = (the_arity_of o) . (x -context_pos_in p) by SORT; :: thesis: verum