per cases ( not S is empty or S is empty ) ;
suppose not S is empty ; :: thesis: for b1 being Element of S holds b1 is FinSequence of D
hence for b1 being Element of S holds b1 is FinSequence of D by Def3; :: thesis: verum
end;
suppose S is empty ; :: thesis: for b1 being Element of S holds b1 is FinSequence of D
then S = <*> D ;
hence for b1 being Element of S holds b1 is FinSequence of D by SUBSET_1:def 1; :: thesis: verum
end;
end;