let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty 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; :: thesis: for X being non-empty 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 non-empty ManySortedSet of the carrier of S; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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]) = {} ; :: according to MSAFREE5:def 21 :: thesis: ( not t is x0 -omitting or C -sub t is x0 -omitting )
assume Z2: Coim (t,[x0,s0]) = {} ; :: according to MSAFREE5:def 21 :: thesis: C -sub t is x0 -omitting
assume Coim ((C -sub t),[x0,s0]) <> {} ; :: according to MSAFREE5:def 21 :: thesis: 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;

A5: now :: thesis: for q being Node of C
for r being Node of t holds
( not q in Leaves (dom C) or not C . q = [x,s] or not a = q ^ r )

given q being Node of C, r being Node of t such that B1: ( q in Leaves (dom C) & C . q = [x,s] & a = q ^ r ) ; :: thesis: contradiction
(C -sub t) . a = t . r by A1, B1, TREES_4:def 7;
hence contradiction by Z2, A3, FUNCT_1:def 7; :: thesis: verum

end;

per cases ( ( a in dom C & C . a <> [x,s] ) or ( a in dom C & C . a = [x,s] ) or ex q being Node of C ex r being Node of t st
( q in Leaves (dom C) & C . q = [x,s] & a = q ^ r ) ) by A1, TREES_4:def 7;

suppose B3: ( a in dom C & C . a <> [x,s] ) ; :: thesis: contradiction

then (C -sub t) . a = C . a by A1, TREES_4:def 7;
hence contradiction by Z1, A3, B3, FUNCT_1:def 7; :: thesis: verum

end;

suppose B2: ( a in dom C & C . a = [x,s] ) ; :: thesis: contradiction

then reconsider q = a as Node of C ;
reconsider r = {} as Node of t by TREES_1:22;
( q ^ r = a & q in Leaves (dom C) ) by B2, Lem13;
hence contradiction by A5, B2; :: thesis: verum

end;

suppose ex q being Node of C ex r being Node of t st
( q in Leaves (dom C) & C . q = [x,s] & a = q ^ r ) ; :: thesis: contradiction

hence contradiction by A5; :: thesis: verum

end;

end;