per cases ( not S is empty or S is empty ) ;

suppose not S is empty ; :: thesis: for b₁ being Element of S holds b₁ is FinSequence of D

hence for b₁ being Element of S holds b₁ is FinSequence of D by Def3; :: thesis: verum

end;

suppose S is empty ; :: thesis: for b₁ being Element of S holds b₁ is FinSequence of D

then S = <*> D ;
hence for b₁ being Element of S holds b₁ is FinSequence of D by SUBSET_1:def 1; :: thesis: verum

end;

end;