let i1, i2 be Element of NAT ; :: thesis: ( ( ex f being homogeneous Function st f in rng F & ( for f being homogeneous Function st f in rng F holds
i1 = arity f ) & ( for f being homogeneous Function st f in rng F holds
i2 = arity f ) implies i1 = i2 ) & ( ( for f being homogeneous Function holds not f in rng F ) & i1 = 0 & i2 = 0 implies i1 = i2 ) )
hereby :: thesis: ( ( for f being homogeneous Function holds not f in rng F ) & i1 = 0 & i2 = 0 implies i1 = i2 )
given f being homogeneous Function such that A10: f in rng F ; :: thesis: ( ( for f being homogeneous Function st f in rng F holds
i1 = arity f ) & ( for f being homogeneous Function st f in rng F holds
i2 = arity f ) implies i1 = i2 )
assume for f being homogeneous Function st f in rng F holds
i1 = arity f ; :: thesis: ( ( for f being homogeneous Function st f in rng F holds
i2 = arity f ) implies i1 = i2 )
then i1 = arity f by A10;
hence ( ( for f being homogeneous Function st f in rng F holds
i2 = arity f ) implies i1 = i2 ) by A10; :: thesis: verum
end;
thus ( ( for f being homogeneous Function holds not f in rng F ) & i1 = 0 & i2 = 0 implies i1 = i2 ) ; :: thesis: verum