set PTA = ParsedTermsOSA X;
set SO = the Sorts of (ParsedTermsOSA X);
deffunc H₁( Element of S) -> Subset of (the Sorts of (ParsedTermsOSA X) . $1) = PTVars $1,X;
consider f being Function such that
A1: ( dom f = the carrier of S & ( for s being Element of S holds f . s = H₁(s) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of by A1, PARTFUN1:def 4, RELAT_1:def 18;
f c= the Sorts of (ParsedTermsOSA X)

proof

let x be set ; :: according to PBOOLE:def 5 :: thesis: ( not x in the carrier of S or f . x c= the Sorts of (ParsedTermsOSA X) . x )
assume x in the carrier of S ; :: thesis: f . x c= the Sorts of (ParsedTermsOSA X) . x
then reconsider s = x as Element of S ;
( f . s = PTVars s,X & PTVars s,X c= the Sorts of (ParsedTermsOSA X) . s ) by A1;
hence f . x c= the Sorts of (ParsedTermsOSA X) . x ; :: thesis: verum

end;

then reconsider f = f as MSSubset of (ParsedTermsOSA X) by PBOOLE:def 23;
take f ; :: thesis: for s being Element of S holds f . s = PTVars s,X
thus for s being Element of S holds f . s = PTVars s,X by A1; :: thesis: verum