deffunc H_{1}( SortSymbol of S) -> set = meet (SubSort (A,$1));

consider f being Function such that

A1: ( dom f = the carrier of S & ( for s being SortSymbol of S holds f . s = H_{1}(s) ) )
from FUNCT_1:sch 4();

reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

f c= the Sorts of U0

take f ; :: thesis: for s being SortSymbol of S holds f . s = meet (SubSort (A,s))

thus for s being SortSymbol of S holds f . s = meet (SubSort (A,s)) by A1; :: thesis: verum

consider f being Function such that

A1: ( dom f = the carrier of S & ( for s being SortSymbol of S holds f . s = H

reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

f c= the Sorts of U0

proof

then reconsider f = f as MSSubset of U0 by PBOOLE:def 18;
reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;

let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S or f . x c= the Sorts of U0 . x )

A2: ( A c= u0 & Constants U0 c= u0 ) by PBOOLE:def 18;

assume x in the carrier of S ; :: thesis: f . x c= the Sorts of U0 . x

then reconsider s = x as SortSymbol of S ;

u0 is opers_closed by Th3;

then u0 in SubSort A by A2, Th13;

then A3: the Sorts of U0 . s in SubSort (A,s) by Def13;

f . s = meet (SubSort (A,s)) by A1;

hence f . x c= the Sorts of U0 . x by A3, SETFAM_1:3; :: thesis: verum

end;let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S or f . x c= the Sorts of U0 . x )

A2: ( A c= u0 & Constants U0 c= u0 ) by PBOOLE:def 18;

assume x in the carrier of S ; :: thesis: f . x c= the Sorts of U0 . x

then reconsider s = x as SortSymbol of S ;

u0 is opers_closed by Th3;

then u0 in SubSort A by A2, Th13;

then A3: the Sorts of U0 . s in SubSort (A,s) by Def13;

f . s = meet (SubSort (A,s)) by A1;

hence f . x c= the Sorts of U0 . x by A3, SETFAM_1:3; :: thesis: verum

take f ; :: thesis: for s being SortSymbol of S holds f . s = meet (SubSort (A,s))

thus for s being SortSymbol of S holds f . s = meet (SubSort (A,s)) by A1; :: thesis: verum