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 A1: ( ( for j being Element of J holds n = arity (O . j) ) & ( for j being Element of J holds m = arity (O . j) ) ) ; :: thesis: n = m
consider j being Element of J;
( n = arity (O . j) & m = arity (O . j) ) by A1;
hence n = m ; :: thesis: verum