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