consider o being OperSymbol of S such that
A1: s in rng (the_arity_of o) by SR;
take o ; :: thesis: o is s -dependent
thus s in rng (the_arity_of o) by A1; :: according to MSAFREE5:def 25 :: thesis: verum