set j = the Element of J;

let n, m be Nat; :: thesis: ( ( for j being Element of J holds n = arity (O . j) ) & ( for j being Element of J holds m = arity (O . j) ) implies n = m )

assume that

A1: for j being Element of J holds n = arity (O . j) and

A2: for j being Element of J holds m = arity (O . j) ; :: thesis: n = m

n = arity (O . the Element of J) by A1;

hence n = m by A2; :: thesis: verum

let n, m be Nat; :: thesis: ( ( for j being Element of J holds n = arity (O . j) ) & ( for j being Element of J holds m = arity (O . j) ) implies n = m )

assume that

A1: for j being Element of J holds n = arity (O . j) and

A2: for j being Element of J holds m = arity (O . j) ; :: thesis: n = m

n = arity (O . the Element of J) by A1;

hence n = m by A2; :: thesis: verum