let f, g be non empty to-naturals homogeneous from-natural-fseqs len-total Function; :: thesis: ( arity f = 0 & arity g = 0 & f . {} = g . {} implies f = g )
assume A1: ( arity f = 0 & arity g = 0 & f . {} = g . {} ) ; :: thesis: f = g
( f is non empty quasi_total Element of HFuncs NAT & g is non empty quasi_total Element of HFuncs NAT ) by Th32;
hence f = g by A1, Th51; :: thesis: verum