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 C being context of x holds
( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )
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 C being context of x holds
( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for C being context of x holds
( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )
let x be Element of X . s; :: thesis: for C being context of x holds
( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )
let C be context of x; :: thesis: ( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )

per cases ( ex s being SortSymbol of S ex x being Element of X . s st C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st C = o -term p ) by Th16;

suppose ex s being SortSymbol of S ex x being Element of X . s st C = x -term ; :: thesis: ( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )

then consider s0 being SortSymbol of S, y being Element of X . s0 such that
A1: C = y -term ;
( s0 = s & x = y ) by A1, Th27;
hence ( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) ) by A1; :: thesis: verum

end;

suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st C = o -term p ; :: thesis: ( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )

then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A2: C = o -term p ;
thus ( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) ) by A2, Th53; :: thesis: verum

end;

end;