set A = Polish-arity V;
set B = (U --> 0) +* (Polish-arity V);
A1: dom ((U --> 0) +* (Polish-arity V)) = (dom (U --> 0)) \/ (dom (Polish-arity V)) by FUNCT_4:def 1
.= U \/ T by FUNCT_2:def 1
.= U by Def9, XBOOLE_1:12 ;
A0: rng (Polish-arity V) c= rng ((U --> 0) +* (Polish-arity V)) by FUNCT_4:18;
0 in rng (Polish-arity V) by FREEALG:def 2;
then (U --> 0) +* (Polish-arity V) is with_zero by A0;
then (U --> 0) +* (Polish-arity V) is Polish-arity-function by A1, Def2;
then reconsider B = (U --> 0) +* (Polish-arity V) as Polish-arity-function of U by A1, Th1;
take W = Polish-WFF-set (U,B); :: thesis: W is (V)
thus Polish-arity V c= Polish-arity W by FUNCT_4:25; :: according to POLNOT_2:def 19 :: thesis: verum