let J be non empty set ; :: thesis: for B being non-empty ManySortedSet of J
for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
let B be non-empty ManySortedSet of J; :: thesis: for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
let O be ManySortedOperation of B; :: thesis: ( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
thus ( O is equal-arity implies for i, j being Element of J holds arity (O . i) = arity (O . j) ) :: thesis: ( ( for i, j being Element of J holds arity (O . i) = arity (O . j) ) implies O is equal-arity )

proof

assume A1: O is equal-arity ; :: thesis: for i, j being Element of J holds arity (O . i) = arity (O . j)
let i, j be Element of J; :: thesis: arity (O . i) = arity (O . j)
A2: dom (O . j) = (arity (O . j)) -tuples_on (B . j) by MARGREL1:22;
( dom O = J & dom (O . i) = (arity (O . i)) -tuples_on (B . i) ) by MARGREL1:22, PARTFUN1:def 2;
hence arity (O . i) = arity (O . j) by A1, A2; :: thesis: verum

end;

assume A3: for i, j being Element of J holds arity (O . i) = arity (O . j) ; :: thesis: O is equal-arity
let x, y be set ; :: according to PRALG_1:def 18 :: thesis: ( x in dom O & y in dom O implies for f, g being Function st O . x = f & O . 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 ( x in dom O & y in dom O ) ; :: thesis: for f, g being Function st O . x = f & O . 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 PARTFUN1:def 2;
let f, g be Function; :: thesis: ( O . x = f & O . y = g implies 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: O . x = f and
A5: O . y = g ; :: thesis: 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
arity (O . x1) = arity (O . y1) by A3;
then A6: dom g = (arity (O . x1)) -tuples_on (B . y1) by A5, MARGREL1:22;
let n, m be Nat; :: thesis: 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
let X, Y be non empty set ; :: thesis: ( dom f = n -tuples_on X & dom g = 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 f = o1 & g = o2 holds
arity o1 = arity o2 )
assume that
A7: dom f = n -tuples_on X and
A8: dom g = 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 f = o1 & g = o2 holds
arity o1 = arity o2
dom f = (arity (O . x1)) -tuples_on (B . x1) by A4, MARGREL1:22;
then A9: n = arity (O . x1) by A7, FINSEQ_2:110;
set p = the Element of n -tuples_on X;
set q = the Element of m -tuples_on Y;
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 f = o1 & g = o2 holds
arity o1 = arity o2
let o2 be non empty homogeneous quasi_total PartFunc of (Y *),Y; :: thesis: ( f = o1 & g = o2 implies arity o1 = arity o2 )
assume that
A10: f = o1 and
A11: g = o2 ; :: thesis: arity o1 = arity o2
A12: arity o2 = len the Element of m -tuples_on Y by A8, A11, MARGREL1:def 25
.= m by CARD_1:def 7 ;
arity o1 = len the Element of n -tuples_on X by A7, A10, MARGREL1:def 25
.= n by CARD_1:def 7 ;
hence arity o1 = arity o2 by A8, A6, A9, A12, FINSEQ_2:110; :: thesis: verum