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] by Th53;
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