defpred S1[ object , object ] means B in B . J;
A1:
for x being object st x in J holds
ex y being object st S1[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
S1[x,f . x] ) )
from CLASSES1:sch 1(A1);
deffunc H1( 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 = H1(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
then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def 6;
then reconsider F = F as ManySortedOperation of B by Def15;
take
F
; 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 ;
( 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
;
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;
( 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
;
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;
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 o2let X,
Y be non
empty set ;
( 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
;
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;
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds
arity o1 = arity o2let o2 be non
empty homogeneous quasi_total PartFunc of
(Y *),
Y;
( g = o1 & h = o2 implies arity o1 = arity o2 )
assume that A8:
g = o1
and A9:
h = o2
;
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;
verum
end;
hence
F is equal-arity
; verum