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 l being Element of (Free (S,Z))
for k, k1 being Element of Args (o,(Free (S,Z)))
for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1
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 l being Element of (Free (S,Z))
for k, k1 being Element of Args (o,(Free (S,Z)))
for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1
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 l being Element of (Free (S,Z))
for k, k1 being Element of Args (o,(Free (S,Z)))
for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1
let Z be non-trivial ManySortedSet of the carrier of S; :: thesis: for z being Element of Z . s
for l being Element of (Free (S,Z))
for k, k1 being Element of Args (o,(Free (S,Z)))
for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1
let z be Element of Z . s; :: thesis: for l being Element of (Free (S,Z))
for k, k1 being Element of Args (o,(Free (S,Z)))
for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1
let l be Element of (Free (S,Z)); :: thesis: for k, k1 being Element of Args (o,(Free (S,Z)))
for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1
let k, k1 be Element of Args (o,(Free (S,Z))); :: thesis: for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1
let C9 be context of z; :: thesis: ( C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) implies C9 -sub l = o -term k1 )
set C = C9;
set p = k;
set p1 = k1;
set x = z;
set t = l;
set X = Z;
assume Z0: C9 = o -term k ; :: thesis: ( not z -context_in k = z -term or not k1 = k +* ((z -context_pos_in k),l) or C9 -sub l = o -term k1 )
assume Z1: z -context_in k = z -term ; :: thesis: ( not k1 = k +* ((z -context_pos_in k),l) or C9 -sub l = o -term k1 )
assume Z2: k1 = k +* ((z -context_pos_in k),l) ; :: thesis: C9 -sub l = o -term k1
set i = z -context_pos_in k;
A1: k is z -context_including by Z0, Th53;
then A2: ( z -context_pos_in k in dom k & dom k = dom (the_arity_of o) & k . (z -context_pos_in k) = z -term ) by Z1, Th71, MSUALG_3:6;
k1 . (z -context_pos_in k) = l by A1, Z2, Th71, FUNCT_7:31;
then ( l in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. (z -context_pos_in k)) & z -term in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. (z -context_pos_in k)) ) by A2, MSUALG_6:2;
then A3: ( the_sort_of l = (the_arity_of o) /. (z -context_pos_in k) & (the_arity_of o) /. (z -context_pos_in k) = the_sort_of (z -context_in k) & the_sort_of (z -context_in k) = s ) by Z1, SORT;
then (z -context_in k) -sub l = l by Z1, Th41;
hence C9 -sub l = o -term k1 by Z0, Z2, A3, Th43, Th53; :: thesis: verum