let S be non empty non void ManySortedSign ; :: thesis: for s, s1 being SortSymbol 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 st the_sort_of C9 = s1 holds
for z1 being b₄ -different Element of Z . s1
for C1 being b₄ -omitting context of z1 holds C1 -sub C9 is context of z
let s, s1 be SortSymbol 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 st the_sort_of C9 = s1 holds
for z1 being b₂ -different Element of Z . s1
for C1 being b₂ -omitting context of z1 holds C1 -sub C9 is context of z
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 st the_sort_of C9 = s1 holds
for z1 being b₁ -different Element of Z . s1
for C1 being b₁ -omitting context of z1 holds C1 -sub C9 is context of z
let z be Element of Z . s; :: thesis: for C9 being context of z st the_sort_of C9 = s1 holds
for z1 being z -different Element of Z . s1
for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z
let C9 be context of z; :: thesis: ( the_sort_of C9 = s1 implies for z1 being z -different Element of Z . s1
for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z )
assume A1: the_sort_of C9 = s1 ; :: thesis: for z1 being z -different Element of Z . s1
for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z
let z1 be z -different Element of Z . s1; :: thesis: for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z
defpred S₁[ Element of (Free (S,Z))] means ( $1 is z -omitting implies ($1,[z1,s1]) <- C9 is context of z );
A2: S₁[z1 -term ] ;
A3: for o being OperSymbol of S
for k being Element of Args (o,(Free (S,Z))) st k is z1 -context_including & S₁[z1 -context_in k] holds
for C being context of z1 st C = o -term k holds
S₁[C]

proof

let o be OperSymbol of S; :: thesis: for k being Element of Args (o,(Free (S,Z))) st k is z1 -context_including & S₁[z1 -context_in k] holds
for C being context of z1 st C = o -term k holds
S₁[C]
let k be Element of Args (o,(Free (S,Z))); :: thesis: ( k is z1 -context_including & S₁[z1 -context_in k] implies for C being context of z1 st C = o -term k holds
S₁[C] )
set p = k;
assume that
A2: k is z1 -context_including and
A3: S₁[z1 -context_in k] ; :: thesis: for C being context of z1 st C = o -term k holds
S₁[C]
let C be context of z1; :: thesis: ( C = o -term k implies S₁[C] )
assume AA: C = o -term k ; :: thesis: S₁[C]
assume c: C is z -omitting ; :: thesis: (C,[z1,s1]) <- C9 is context of z
set t = C9;
deffunc H₁( Nat) -> set = ((k /. $1),[z1,s1]) <- C9;
consider q being FinSequence such that
A4: ( len q = len k & ( for i being Nat st i in dom q holds
q . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A5: ( dom q = dom k & dom k <> {} ) by A2, A4, FINSEQ_3:29;
then A6: ( not k is empty & not q is empty ) ;
A8: dom k = dom (the_arity_of o) by MSUALG_6:2;
then A9: len q = len (the_arity_of o) by A5, FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom q holds
q . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i)

let i be Nat; :: thesis: ( i in dom q implies q . b₁ in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b₁) )
assume B1: i in dom q ; :: thesis: q . b₁ in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b₁)
then B2: k /. i = k . i by A5, PARTFUN1:def 6;

per cases ( z1 -context_pos_in k = i or z1 -context_pos_in k <> i ) ;

suppose z1 -context_pos_in k = i ; :: thesis: q . b₁ in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b₁)

then B3: ( z1 -context_in k = k . i & q . i = H₁(i) & k /. i is z -omitting ) by c, AA, A5, A4, A2, Th71, Th54;
k . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i) by B1, A5, A8, MSUALG_6:2;
then the_sort_of (z1 -context_in k) = (the_arity_of o) /. i by B3, SORT;
hence q . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i) by A1, B2, B3, aaa1; :: thesis: verum

end;

suppose z1 -context_pos_in k <> i ; :: thesis: q . b₁ in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b₁)

then k /. i is z1 -omitting by A2, A5, B1, Th72;
then ( q . i = H₁(i) & H₁(i) = k . i ) by A4, B1, B2, Th23;
hence q . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i) by B1, A5, A8, MSUALG_6:2; :: thesis: verum

end;

end;

end;

then reconsider q = q as Element of Args (o,(Free (S,Z))) by A9, MSAFREE2:5;

now :: thesis: for i being Nat
for d1 being DecoratedTree st i in dom k & d1 = k . i holds
q . i = (d1,[z1,s1]) <- C9

let i be Nat; :: thesis: for d1 being DecoratedTree st i in dom k & d1 = k . i holds
q . i = (d1,[z1,s1]) <- C9
let d1 be DecoratedTree; :: thesis: ( i in dom k & d1 = k . i implies q . i = (d1,[z1,s1]) <- C9 )
assume ( i in dom k & d1 = k . i ) ; :: thesis: q . i = (d1,[z1,s1]) <- C9
then ( q . i = H₁(i) & k /. i = d1 ) by A4, A5, PARTFUN1:def 6;
hence q . i = (d1,[z1,s1]) <- C9 ; :: thesis: verum

end;

then A7: ((o -term k),[z1,s1]) <- C9 = [o, the carrier of S] -tree q by A5, A6, ThL8
.= o -term q ;
q is z -context_including

proof

take i = z1 -context_pos_in k; :: according to MSAFREE5:def 24 :: thesis: ( i in dom q & q . i is context of z & ( for j being Nat
for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting ) )
thus i in dom q by A2, A5, Th71; :: thesis: ( q . i is context of z & ( for j being Nat
for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting ) )
then B2: k /. i = k . i by A5, PARTFUN1:def 6;
( z1 -context_in k = k . i & q . i = H₁(i) & k /. i is z -omitting ) by c, AA, A5, A4, A2, Th71, Th54;
hence q . i is context of z by B2, A3; :: thesis: for j being Nat
for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting
let j be Nat; :: thesis: for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting
let q1 be Element of (Free (S,Z)); :: thesis: ( j in dom q & j <> i & q1 = q . j implies q1 is z -omitting )
assume B4: ( j in dom q & j <> i & q1 = q . j ) ; :: thesis: q1 is z -omitting
then B5: k /. j = k . j by A5, PARTFUN1:def 6;
k /. j is z1 -omitting by A2, B4, A5, Th72;
then ( q1 = H₁(j) & H₁(j) = k . j ) by B4, A4, B5, Th23;
hence q1 is z -omitting by c, B5, B4, A5, AA, Th54; :: thesis: verum

end;

hence (C,[z1,s1]) <- C9 is context of z by AA, A7, Th53; :: thesis: verum

end;

let C1 be z -omitting context of z1; :: thesis: C1 -sub C9 is context of z
S₁[C1] from MSAFREE5:sch 4(A2, A3);
hence C1 -sub C9 is context of z by A1, SUB; :: thesis: verum