rng e = U /\ {} ;
then reconsider ee = e as U -valued 0 -element FinSequence by RELAT_1:def 19;
for X being set holds (X SubstWith u) . ee is 0 -element ;
hence for b₁ being set st b₁ = (x SubstWith u) . e holds
b₁ is empty ; :: thesis: verum