defpred S₁[ object , object ] means B in B . J;
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 . J)) .--> (f . J);
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;

now :: 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

end;

then reconsider F = F as ManySortedOperation of B by Def15;
take F ; :: thesis: F is equal-arity
for x, y being set st x in dom F & y in dom F holds
for f, g being Function st F . x = f & F . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2

proof

let x, y be set ; :: thesis: ( x in dom F & y in dom F implies for f, g being Function st F . x = f & F . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2 )
assume that
A4: x in dom F and
A5: y in dom F ; :: thesis: for f, g being Function st F . x = f & F . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2
reconsider x1 = x, y1 = y as Element of J by A3, A4, A5;
let g, h be Function; :: thesis: ( F . x = g & F . y = h implies for n, m being Nat
for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2 )
assume that
A6: F . x = g and
A7: F . y = h ; :: thesis: for n, m being Nat
for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
reconsider fx = f . x1 as Element of B . x1 by A2;
let n, m be Nat; :: thesis: for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
let X, Y be non empty set ; :: thesis: ( dom g = n -tuples_on X & dom h = m -tuples_on Y implies for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2 )
assume that
dom g = n -tuples_on X and
dom h = m -tuples_on Y ; :: thesis: for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
let o1 be non empty homogeneous quasi_total PartFunc of (X *),X; :: thesis: for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2
let o2 be non empty homogeneous quasi_total PartFunc of (Y *),Y; :: thesis: ( g = o1 & h = o2 implies arity o1 = arity o2 )
assume that
A8: g = o1 and
A9: h = o2 ; :: thesis: arity o1 = arity o2
reconsider o1x = (<*> (B . x1)) .--> fx as non empty homogeneous quasi_total PartFunc of ((B . x1) *),(B . x1) by MARGREL1:18;
consider p1 being object such that
A11: p1 in dom o1 by XBOOLE_0:def 1;
dom o1 c= X * by RELAT_1:def 18;
then reconsider p1 = p1 as Element of X * by A11;
o1 = (<*> (B . x)) .--> (f . x) by A3, A4, A6, A8;
then p1 = <*> (B . x1) by A11, TARSKI:def 1;
then len p1 = 0 ;
then A12: arity o1 = 0 by A11, MARGREL1:def 25;
reconsider fy = f . y1 as Element of B . y1 by A2;
reconsider o2y = (<*> (B . y1)) .--> fy as non empty homogeneous quasi_total PartFunc of ((B . y1) *),(B . y1) by MARGREL1:18;
consider p2 being object such that
A14: p2 in dom o2 by XBOOLE_0:def 1;
dom o2 c= Y * by RELAT_1:def 18;
then reconsider p2 = p2 as Element of Y * by A14;
o2 = (<*> (B . y)) .--> (f . y) by A3, A5, A7, A9;
then p2 = <*> (B . y1) by A14, TARSKI:def 1;
then len p2 = 0 ;
hence arity o1 = arity o2 by A12, A14, MARGREL1:def 25; :: thesis: verum

end;

hence F is equal-arity ; :: thesis: verum