defpred S₁[ object , object ] means $2 in B . $1;
A1: for x being object st x in J holds
ex y being object st S₁[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₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
deffunc H₁( 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₁(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

proof

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;

then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def 6;
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