thus ( F is Polish-arity-like implies ( dom F is Polish-language & F is natural-valued & F is with_zero ) ) :: thesis: ( dom F is Polish-language & F is natural-valued & F is with_zero implies F is Polish-arity-like )

proof

assume F is Polish-arity-like ; :: thesis: ( dom F is Polish-language & F is natural-valued & F is with_zero )
then consider T being Polish-language such that
A1: F is Polish-arity-function of T ;
reconsider A = F as Polish-arity-function of T by A1;
dom A = T by FUNCT_2:def 1;
hence dom F is Polish-language ; :: thesis: ( F is natural-valued & F is with_zero )
rng A c= NAT by RELAT_1:def 19;
hence F is natural-valued ; :: thesis: F is with_zero
consider a being object such that
A5: ( a in T & A . a = 0 ) by POLNOT_1:def 18;
0 in rng F by A5, FUNCT_2:4;
hence F is with_zero ; :: thesis: verum

end;

assume that
A10: dom F is Polish-language and
A11: F is natural-valued and
A12: F is with_zero ; :: thesis: F is Polish-arity-like
reconsider T = dom F as Polish-language by A10;
reconsider F = F as Function of T,NAT by A11, FUNCT_2:2;
0 in rng F by A12, FREEALG:def 2;
then ex a being object st
( a in T & F . a = 0 ) by FUNCT_1:def 3;
then F is Polish-arity-function of T by POLNOT_1:def 18;
hence F is Polish-arity-like ; :: thesis: verum