set f = the ManySortedSet of J;
deffunc H₁( object ) -> Element of bool [:(S . $1),{ the ManySortedSet of J}:] = (S . $1) --> the ManySortedSet of J;
consider X being ManySortedSet of I such that
A1: for x being object st x in I holds
X . x = H₁(x) from PBOOLE:sch 4();
X is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 X or X . x is set )
assume x in dom X ; :: thesis: X . x is set
then x in I by PARTFUN1:def 2;
then X . x = H₁(x) by A1;
hence X . x is set ; :: thesis: verum

end;

then reconsider X = X as ManySortedFunction of I ;
take X ; :: thesis: for i, j being set st i in I holds
( dom (X . i) = S . i & ( j in S . i implies (X . i) . j is ManySortedSet of J ) )
let i, j be set ; :: thesis: ( i in I implies ( dom (X . i) = S . i & ( j in S . i implies (X . i) . j is ManySortedSet of J ) ) )
assume A2: i in I ; :: thesis: ( dom (X . i) = S . i & ( j in S . i implies (X . i) . j is ManySortedSet of J ) )
then X . i = H₁(i) by A1;
hence dom (X . i) = S . i ; :: thesis: ( j in S . i implies (X . i) . j is ManySortedSet of J )
assume j in S . i ; :: thesis: (X . i) . j is ManySortedSet of J
then ( X . i = H₁(i) & H₁(i) . j = the ManySortedSet of J ) by A1, A2, FUNCOP_1:7;
hence (X . i) . j is ManySortedSet of J ; :: thesis: verum