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

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 . 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_{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: 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

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

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

then reconsider F = F as ManySortedOperation of B by Def15;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;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

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

hence
F is equal-arity
; :: thesis: verum
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;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