let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for o being OperSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let s be SortSymbol of S; :: thesis: for o being OperSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let o be OperSymbol of S; :: thesis: for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let Z be non-trivial ManySortedSet of the carrier of S; :: thesis: for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let z be Element of Z . s; :: thesis: for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let C9 be context of z; :: thesis: for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let w, p be Element of Args (o,(Free (S,Z))); :: thesis: for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let t be Element of (Free (S,Z)); :: thesis: ( w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s implies C9 -sub t = o -term p )
assume that
A1: w is z -context_including and
A2: C9 = o -term w and
A3: p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) and
A4: the_sort_of t = s ; :: thesis: C9 -sub t = o -term p
A5: ( dom p = dom (the_arity_of o) & dom (the_arity_of o) = dom w & dom w <> {} ) by A1, MSUALG_3:6;
then reconsider v = w, q = p as non empty DTree-yielding FinSequence ;

now :: thesis: for i being Nat
for d1 being DecoratedTree st i in dom v & d1 = v . i holds
q . i = (d1,[z,s]) <- t

let i be Nat; :: thesis: for d1 being DecoratedTree st i in dom v & d1 = v . i holds
q . b₂ = (b₃,[z,s]) <- t
let d1 be DecoratedTree; :: thesis: ( i in dom v & d1 = v . i implies q . b₁ = (b₂,[z,s]) <- t )
assume A6: ( i in dom v & d1 = v . i ) ; :: thesis: q . b₁ = (b₂,[z,s]) <- t
A7: (z -context_in w) -sub t = ((z -context_in w),[z,s]) <- t by A4, SUB;

per cases ( i = z -context_pos_in w or i <> z -context_pos_in w ) ;

suppose A8: i = z -context_pos_in w ; :: thesis: q . b₁ = (b₂,[z,s]) <- t

then d1 = z -context_in w by A1, A6, Th71;
hence q . i = (d1,[z,s]) <- t by A3, A6, A7, A8, FUNCT_7:31; :: thesis: verum

end;

suppose A8: i <> z -context_pos_in w ; :: thesis: q . b₁ = (b₂,[z,s]) <- t

then ( w /. i is z -omitting & w /. i = d1 ) by A1, A6, Th72, PARTFUN1:def 6;
then (d1,[z,s]) <- t = d1 by Th23;
hence q . i = (d1,[z,s]) <- t by A3, A6, A8, FUNCT_7:32; :: thesis: verum

end;

end;

end;

then (([o, the carrier of S] -tree v),[z,s]) <- t = [o, the carrier of S] -tree q by A5, ThL8;
hence C9 -sub t = o -term p by A2, A4, SUB; :: thesis: verum