let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in t1 with-replacement ((<*> NAT),t) or p in t ) & ( not p in t or p in t1 with-replacement ((<*> NAT),t) ) )
A3: {} in t1 by TREES_1:22;
then A2: ( p in t1 with-replacement ((<*> NAT),t) iff ( ( p in t1 & not {} is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in t & p = {} ^ r ) ) ) by TREES_1:def 9;

hereby :: thesis: ( not p in t or p in t1 with-replacement ((<*> NAT),t) )

assume p in t1 with-replacement ((<*> NAT),t) ; :: thesis: p in t

per cases then ( {} = p or ex r being FinSequence of NAT st
( r in t & p = {} ^ r ) ) by A2, XBOOLE_1:61;

suppose {} = p ; :: thesis: p in t

hence p in t by TREES_1:22; :: thesis: verum

end;

suppose ex r being FinSequence of NAT st
( r in t & p = {} ^ r ) ; :: thesis: p in t

hence p in t ; :: thesis: verum

end;

end;

end;

assume p in t ; :: thesis: p in t1 with-replacement ((<*> NAT),t)
then ( p in t & p = {} ^ p ) ;
hence p in t1 with-replacement ((<*> NAT),t) by A3, TREES_1:def 9; :: thesis: verum