let a be object ; :: thesis: ( a in GRZ-ops implies GRZ-arity . a = GRZ-op-arity . a )
assume A1: a in GRZ-ops ; :: thesis: GRZ-arity . a = GRZ-op-arity . a
then a in GRZ-symbols by XBOOLE_0:def 3;
hence GRZ-arity . a = GRZ-op-arity . a by A1, Def4; :: thesis: verum