set f = the ManySortedSubset of S2;
deffunc H1( object ) -> Element of bool [:(S1 . $1),{ the ManySortedSubset of S2}:] = (S1 . $1) --> the ManySortedSubset of S2;
consider X being ManySortedSet of I such that
A1: for x being object st x in I holds
X . x = H1(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 = H1(x) by A1;
hence X . x is set ; :: thesis: verum
end;
then reconsider X = X as ManySortedFunction of I ;
X is ManySortedMSSet of S1,J
proof
let i, j be set ; :: according to AOFA_A00:def 6 :: thesis: ( i in I implies ( dom (X . i) = S1 . i & ( j in S1 . i implies (X . i) . j is ManySortedSet of J ) ) )
assume A2: i in I ; :: thesis: ( dom (X . i) = S1 . i & ( j in S1 . i implies (X . i) . j is ManySortedSet of J ) )
then X . i = H1(i) by A1;
hence dom (X . i) = S1 . i ; :: thesis: ( j in S1 . i implies (X . i) . j is ManySortedSet of J )
assume j in S1 . i ; :: thesis: (X . i) . j is ManySortedSet of J
then ( X . i = H1(i) & H1(i) . j = the ManySortedSubset of S2 ) by A1, A2, FUNCOP_1:7;
hence (X . i) . j is ManySortedSet of J ; :: thesis: verum
end;
then reconsider X = X as ManySortedMSSet of S1,J ;
take X ; :: thesis: for i, a being set st i in I & a in S1 . i holds
(X . i) . a is ManySortedSubset of S2
let i, j be set ; :: thesis: ( i in I & j in S1 . i implies (X . i) . j is ManySortedSubset of S2 )
assume ( i in I & j in S1 . i ) ; :: thesis: (X . i) . j is ManySortedSubset of S2
then ( X . i = H1(i) & H1(i) . j = the ManySortedSubset of S2 ) by A1, FUNCOP_1:7;
hence (X . i) . j is ManySortedSubset of S2 ; :: thesis: verum