let f, g be non empty NAT * -defined to-naturals homogeneous len-total Function; :: thesis: ( arity f = 0 & arity g = 0 & f . {} = g . {} implies f = g )
A1: g is non empty quasi_total Element of HFuncs NAT by Th28;
f is non empty quasi_total Element of HFuncs NAT by Th28;
hence ( arity f = 0 & arity g = 0 & f . {} = g . {} implies f = g ) by A1, Th46; :: thesis: verum