let S be non empty non void ManySortedSign ; 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; 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; 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; 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; 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))); 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)); ( 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) )
; 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;
hence
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))
by A2, A3, MSAFREE2:5; verum