let x be set ; :: thesis: for D being non empty set holds
( x in (D *) \ {{}} iff ( x is b₁ -valued FinSequence & not x is empty ) )
let D be non empty set ; :: thesis: ( x in (D *) \ {{}} iff ( x is D -valued FinSequence & not x is empty ) )
( ( x is D -valued FinSequence & not x is empty ) iff x is non empty FinSequence of D ) by Lm1;
hence ( x in (D *) \ {{}} iff ( x is D -valued FinSequence & not x is empty ) ) by Th5; :: thesis: verum