defpred S₁[ set , set ] means B in B . J;
A1: for x being set st x in J holds
ex y being set st S₁[x,y] by XBOOLE_0:def 1;
consider f being Function such that
A2: ( dom f = J & ( for x being set st x in J holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
deffunc H₁( set ) -> set = (<*> (B . J)) .--> (f . J);
consider F being Function such that
A3: ( dom F = J & ( for x being set st x in J holds
F . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider F = F as ManySortedSet of by A3, PARTFUN1:def 4, RELAT_1:def 18;
for x being set st x in dom F holds
F . x is Function

proof

let x be set ; :: 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 by FUNCOP_1:def 6;

now

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 UNIALG_1:2; :: 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 A4: ( x in dom F & 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
then reconsider x1 = x, y1 = y as Element of J by A3;
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 A5: ( F . x = g & 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
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 ( dom g = n -tuples_on X & 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 ( g = o1 & h = o2 ) ; :: thesis: arity o1 = arity o2
then A6: ( o1 = (<*> (B . x)) .--> (f . x) & o2 = (<*> (B . y)) .--> (f . y) ) by A3, A4, A5;
reconsider fx = f . x1 as Element of B . x1 by A2;
reconsider fy = f . y1 as Element of B . y1 by A2;
reconsider o1x = (<*> (B . x1)) .--> fx as non empty homogeneous quasi_total PartFunc of ((B . x1) * ),(B . x1) by UNIALG_1:2;
reconsider o2y = (<*> (B . y1)) .--> fy as non empty homogeneous quasi_total PartFunc of ((B . y1) * ),(B . y1) by UNIALG_1:2;
A7: ( dom o1x = {({} (B . x1))} & dom o2y = {({} (B . y1))} ) by FUNCOP_1:19;
consider p1 being set such that
A8: 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 A8;
p1 = <*> (B . x1) by A6, A7, A8, TARSKI:def 1;
then len p1 = 0 ;
then A9: arity o1 = 0 by A8, UNIALG_1:def 10;
consider p2 being set such that
A10: 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 A10;
p2 = <*> (B . y1) by A6, A7, A10, TARSKI:def 1;
then len p2 = 0 ;
hence arity o1 = arity o2 by A9, A10, UNIALG_1:def 10; :: thesis: verum

end;

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