deffunc H2( SortSymbol of S) -> set = { e where e is Element of (Equations S) . $1 : A |= e } ;
consider f being ManySortedSet of S such that
A1: for s being SortSymbol of S holds f . s = H2(s) from PBOOLE:sch 5();
 f is EqualSet of S
proof
let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in the carrier of S or f . x c= (Equations S) . x )
assume x in the carrier of S ; :: thesis: f . x c= (Equations S) . x
then reconsider s = x as SortSymbol of S ;
A2: f . s = H2(s) by A1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f . x or y in (Equations S) . x )
assume y in f . x ; :: thesis: y in (Equations S) . x
then ex e being Element of (Equations S) . s st
( y = e & A |= e ) by A2;
hence y in (Equations S) . x ; :: thesis: verum
end;
hence ex b1 being EqualSet of S st
for s being SortSymbol of S holds b1 . s = { e where e is Element of (Equations S) . s : A |= e } by A1; :: thesis: verum