set k = T | t;
A1: dom (T | t) = (dom T) | t by TREES_2:def 10;

A2: now :: thesis: for u being Element of dom (T | t)
for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = (T | t) . u holds
succ ((T | t),u) = the Enumeration of compn w

let u be Element of dom (T | t); :: thesis: for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = (T | t) . u holds
succ ((T | t),u) = the Enumeration of compn w
reconsider tu = t ^ u as Element of dom T by A1, TREES_1:def 6;
let w be Element of [:(LTLB_WFF **),(LTLB_WFF **):]; :: thesis: ( w = (T | t) . u implies succ ((T | t),u) = the Enumeration of compn w )
assume w = (T | t) . u ; :: thesis: succ ((T | t),u) = the Enumeration of compn w
then A3: w = T . (t ^ u) by A1, TREES_2:def 10;
thus succ ((T | t),u) = succ (T,tu) by TREES_9:31
.= the Enumeration of compn w by Def11, A3 ; :: thesis: verum

end;

(T | t) . {} = T . t by TREES_9:35;
hence T | t is pnptree of T . t by A2, Def11; :: thesis: verum