let T be Polish-language; :: thesis: for B being Polish-arity-function holds
( B is Polish-arity-function of T iff T = dom B )
let B be Polish-arity-function; :: thesis: ( B is Polish-arity-function of T iff T = dom B )
thus ( B is Polish-arity-function of T implies T = dom B ) by FUNCT_2:def 1; :: thesis: ( T = dom B implies B is Polish-arity-function of T )
consider U being Polish-language such that
A1: B is Polish-arity-function of U by Def1;
assume T = dom B ; :: thesis: B is Polish-arity-function of T
hence B is Polish-arity-function of T by A1, FUNCT_2:def 1; :: thesis: verum