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 w being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
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 w being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
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 w being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
let Z be non-trivial ManySortedSet of the carrier of S; :: thesis: for z being Element of Z . s
for w being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
let z be Element of Z . s; :: thesis: for w being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
let w be Element of Args (o,(Free (S,Z))); :: thesis: for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
let t be Element of (Free (S,Z)); :: thesis: ( w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) implies w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z))) )
assume A1: ( w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) ) ; :: thesis: w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
A2: ( dom (w +* ((z -context_pos_in w),t)) = dom w & dom w = dom (the_arity_of o) ) by FUNCT_7:30, MSUALG_6:2;
then A3: len (w +* ((z -context_pos_in w),t)) = len (the_arity_of o) by FINSEQ_3:29;
now :: thesis: for i being Nat st i in dom w holds
(w +* ((z -context_pos_in w),t)) . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i)
let i be Nat; :: thesis: ( i in dom w implies (w +* ((z -context_pos_in w),t)) . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1) )
assume A4: i in dom w ; :: thesis: (w +* ((z -context_pos_in w),t)) . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1)
per cases ( i = z -context_pos_in w or i <> z -context_pos_in w ) ;
suppose i = z -context_pos_in w ; :: thesis: (w +* ((z -context_pos_in w),t)) . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1)
then ( (w +* ((z -context_pos_in w),t)) . i = t & the_sort_of t = (the_arity_of o) /. i ) by A1, A2, A4, PARTFUN1:def 6, FUNCT_7:31;
hence (w +* ((z -context_pos_in w),t)) . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i) by SORT; :: thesis: verum
end;
suppose i <> z -context_pos_in w ; :: thesis: (w +* ((z -context_pos_in w),t)) . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1)
then (w +* ((z -context_pos_in w),t)) . i = w . i by FUNCT_7:32;
hence (w +* ((z -context_pos_in w),t)) . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i) by A2, A4, MSUALG_6:2; :: thesis: verum
end;
end;
end;
hence w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z))) by A2, A3, MSAFREE2:5; :: thesis: verum