let x be set ; :: thesis: for S being Language holds
( x is string of S iff x is non empty FinSequence of AllSymbolsOf S )
let S be Language; :: thesis: ( x is string of S iff x is non empty FinSequence of AllSymbolsOf S )
( x is non empty FinSequence of AllSymbolsOf S iff x is non empty Element of (AllSymbolsOf S) * ) by FINSEQ_1:def 11;
hence ( x is string of S iff x is non empty FinSequence of AllSymbolsOf S ) by Th12; :: thesis: verum