let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x
for s0 being SortSymbol of S
for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds
C -sub t is x0 -omitting
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x
for s0 being SortSymbol of S
for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds
C -sub t is x0 -omitting
let X be V5() ManySortedSet of the carrier of S; for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x
for s0 being SortSymbol of S
for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds
C -sub t is x0 -omitting
let x be Element of X . s; for t being Element of (Free (S,X))
for C being context of x
for s0 being SortSymbol of S
for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds
C -sub t is x0 -omitting
let t be Element of (Free (S,X)); for C being context of x
for s0 being SortSymbol of S
for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds
C -sub t is x0 -omitting
let C be context of x; for s0 being SortSymbol of S
for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds
C -sub t is x0 -omitting
let s0 be SortSymbol of S; for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds
C -sub t is x0 -omitting
let x0 be Element of X . s0; ( the_sort_of t = s & C is x0 -omitting & t is x0 -omitting implies C -sub t is x0 -omitting )
assume
the_sort_of t = s
; ( not C is x0 -omitting or not t is x0 -omitting or C -sub t is x0 -omitting )
then A1:
C -sub t = (C,[x,s]) <- t
by SUB;
assume Z1:
Coim (C,[x0,s0]) = {}
; MSAFREE5:def 21 ( not t is x0 -omitting or C -sub t is x0 -omitting )
assume Z2:
Coim (t,[x0,s0]) = {}
; MSAFREE5:def 21 C -sub t is x0 -omitting
assume
Coim ((C -sub t),[x0,s0]) <> {}
; MSAFREE5:def 21 contradiction
then consider a being object such that
A2:
a in Coim ((C -sub t),[x0,s0])
by XBOOLE_0:7;
A3:
( a in dom (C -sub t) & (C -sub t) . a in {[x0,s0]} )
by A2, FUNCT_1:def 7;
reconsider a = a as Element of dom (C -sub t) by A2, FUNCT_1:def 7;