let J be non empty set ; :: thesis: for B being V2() 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 V2() 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 )

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

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 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 A3:
for i, j being Element of J holds arity (O . i) = arity (O . j)
; :: thesis: O is equal-arity
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;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

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