theorem Th47: :: COMPUT_1:48

for f, g being non empty NAT * -defined to-naturals homogeneous len-total Function st arity f = 0 & arity g = 0 & f . {} = g . {} holds
f = g