let T be Polish-language; for V being full Polish-language of T
for U being T -extending Polish-language holds
not for W being full Polish-language of U holds W is (b1)
let V be full Polish-language of T; for U being T -extending Polish-language holds
not for W being full Polish-language of U holds W is (V)
let U be T -extending Polish-language; not for W being full Polish-language of U holds W is (V)
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); W is (V)
thus
Polish-arity V c= Polish-arity W
by FUNCT_4:25; POLNOT_2:def 19 verum