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 )
assume that
A1: arity f = 0 and
A2: arity g = 0 and
A3: f . {} = g . {} ; :: thesis: f = g
A4: 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 f = g by A1, A2, A3, A4, Th46; :: thesis: verum