defpred S_{1}[ object , object ] means $2 in B . $1;

A1: for x being object st x in J holds

ex y being object st S_{1}[x,y]
by XBOOLE_0:def 1;

consider f being Function such that

A2: ( dom f = J & ( for x being object st x in J holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A1);

deffunc H_{1}( object ) -> set = (<*> (B . $1)) .--> (f . $1);

consider F being Function such that

A3: ( dom F = J & ( for x being object st x in J holds

F . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

reconsider F = F as ManySortedSet of J by A3, PARTFUN1:def 2, RELAT_1:def 18;

for x being object st x in dom F holds

F . x is Function

take F ; :: thesis: for j being Element of J holds F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)

let j be Element of J; :: thesis: F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)

reconsider b = f . j as Element of B . j by A2;

F . j = (<*> (B . j)) .--> b by A3;

hence F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by MARGREL1:18; :: thesis: verum

A1: for x being object st x in J holds

ex y being object st S

consider f being Function such that

A2: ( dom f = J & ( for x being object st x in J holds

S

deffunc H

consider F being Function such that

A3: ( dom F = J & ( for x being object st x in J holds

F . x = H

reconsider F = F as ManySortedSet of J by A3, PARTFUN1:def 2, RELAT_1:def 18;

for x being object st x in dom F holds

F . x is Function

proof

then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def 6;
let x be object ; :: thesis: ( x in dom F implies F . x is Function )

assume x in dom F ; :: thesis: F . x is Function

then F . x = (<*> (B . x)) .--> (f . x) by A3;

hence F . x is Function ; :: thesis: verum

end;assume x in dom F ; :: thesis: F . x is Function

then F . x = (<*> (B . x)) .--> (f . x) by A3;

hence F . x is Function ; :: thesis: verum

take F ; :: thesis: for j being Element of J holds F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)

let j be Element of J; :: thesis: F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)

reconsider b = f . j as Element of B . j by A2;

F . j = (<*> (B . j)) .--> b by A3;

hence F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by MARGREL1:18; :: thesis: verum