let D be non empty set ; :: thesis: for x being set holds
( x is non empty FinSequence of D iff x in (D *) \ {{}} )
let x be set ; :: thesis: ( x is non empty FinSequence of D iff x in (D *) \ {{}} )
thus ( x is non empty FinSequence of D implies x in (D *) \ {{}} ) :: thesis: ( x in (D *) \ {{}} implies x is non empty FinSequence of D )

proof

assume x is non empty FinSequence of D ; :: thesis: x in (D *) \ {{}}
then ( not x in {{}} & x in D * ) by FINSEQ_1:def 11, TARSKI:def 1;
hence x in (D *) \ {{}} by XBOOLE_0:def 5; :: thesis: verum

end;

assume x in (D *) \ {{}} ; :: thesis: x is non empty FinSequence of D
then ( x in D * & not x in {{}} ) by XBOOLE_0:def 5;
hence x is non empty FinSequence of D by FINSEQ_1:def 11, TARSKI:def 1; :: thesis: verum