set f = the ManySortedSubset of S2;

deffunc H_{1}( 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 = H_{1}(x)
from PBOOLE:sch 4();

X is Function-yielding

X is 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 = H_{1}(i) & H_{1}(i) . j = the ManySortedSubset of S2 )
by A1, FUNCOP_1:7;

hence (X . i) . j is ManySortedSubset of S2 ; :: thesis: verum

deffunc H

consider X being ManySortedSet of I such that

A1: for x being object st x in I holds

X . x = H

X is Function-yielding

proof

then reconsider X = X as ManySortedFunction of I ;
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_{1}(x)
by A1;

hence X . x is set ; :: thesis: verum

end;assume x in dom X ; :: thesis: X . x is set

then x in I by PARTFUN1:def 2;

then X . x = H

hence X . x is set ; :: thesis: verum

X is ManySortedMSSet of S1,J

proof

then reconsider X = X as ManySortedMSSet of S1,J ;
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 = H_{1}(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 = H_{1}(i) & H_{1}(i) . j = the ManySortedSubset of S2 )
by A1, A2, FUNCOP_1:7;

hence (X . i) . j is ManySortedSet of J ; :: thesis: verum

end;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 = H

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 = H

hence (X . i) . j is ManySortedSet of J ; :: thesis: verum

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 = H

hence (X . i) . j is ManySortedSubset of S2 ; :: thesis: verum