set f = the ManySortedSet of J;

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

X is Function-yielding

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_{1}(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_{1}(i) & H_{1}(i) . j = the ManySortedSet of J )
by A1, A2, FUNCOP_1:7;

hence (X . i) . j is ManySortedSet of J ; :: 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

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

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

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