let S be non empty non void ManySortedSign ; :: thesis:
let s be SortSymbol of S; :: thesis:
let X be V5() ManySortedSet of the carrier of S; :: thesis:
let x be Element of X . s; :: thesis:
let C be context of x; :: thesis:

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:

end;

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:

end;