set i = the Element of J;
take arity (O . the Element of J) ; :: thesis: for j being Element of J holds arity (O . the Element of J) = arity (O . j)
let j be Element of J; :: thesis: arity (O . the Element of J) = arity (O . j)
thus arity (O . the Element of J) = arity (O . j) by Th11; :: thesis: verum