let D be non empty set ; :: thesis: for x being set holds
( x in (D *) \ {{}} iff ( x is D -valued FinSequence & not x is empty ) )
let x be 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 Lm45;
hence ( x in (D *) \ {{}} iff ( x is D -valued FinSequence & not x is empty ) ) by Lm2; :: thesis: verum