let J be non empty set ; :: thesis: for B being V2() ManySortedSet of
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 V2() ManySortedSet of ; :: 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 by PARTFUN1:def 4;
( dom (O . i) = (arity (O . i)) -tuples_on (B . i) & dom (O . j) = (arity (O . j)) -tuples_on (B . j) ) by UNIALG_2:2;
hence arity (O . i) = arity (O . j) by A1, A2, Def16; :: 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 16 :: 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 A4: ( 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
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 A5: ( O . x = f & 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
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 A6: ( dom f = n -tuples_on X & 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
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 A7: ( f = o1 & g = o2 ) ; :: thesis: arity o1 = arity o2
reconsider x1 = x, y1 = y as Element of J by A4, PARTFUN1:def 4;
arity (O . x1) = arity (O . y1) by A3;
then ( dom f = (arity (O . x1)) -tuples_on (B . x1) & dom g = (arity (O . x1)) -tuples_on (B . y1) ) by A5, UNIALG_2:2;
then A8: ( n = arity (O . x1) & m = arity (O . x1) ) by A6, Th1;
consider p being Element of n -tuples_on X;
A9: arity o1 = len p by A6, A7, UNIALG_1:def 10
.= n by FINSEQ_1:def 18 ;
consider q being Element of m -tuples_on Y;
arity o2 = len q by A6, A7, UNIALG_1:def 10
.= m by FINSEQ_1:def 18 ;
hence arity o1 = arity o2 by A8, A9; :: thesis: verum