per cases ( not phi is 0wff or phi is 0wff ) ;

suppose not phi is 0wff ; :: thesis: (SubWffsOf phi) `2 is Element of (AllSymbolsOf S) *

then consider phi1 being wff string of S, p being FinSequence such that
C0: ( p is AllSymbolsOf S -valued & SubWffsOf phi = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) by DefSub1;
((SubWffsOf phi) `2) \+\ p = {} by C0;
then ( (SubWffsOf phi) `2 = p & p is FinSequence of AllSymbolsOf S ) by C0, FOMODEL0:26, FOMODEL0:29;
hence (SubWffsOf phi) `2 is Element of (AllSymbolsOf S) * by FINSEQ_1:def 11; :: thesis: verum

end;

suppose phi is 0wff ; :: thesis: (SubWffsOf phi) `2 is Element of (AllSymbolsOf S) *

then SubWffsOf phi = [phi,{}] by DefSub1;
then ((SubWffsOf phi) `2) \+\ {} = {} null (AllSymbolsOf S) ;
then reconsider ITT = (SubWffsOf phi) `2 as AllSymbolsOf S -valued FinSequence ;
ITT is FinSequence of AllSymbolsOf S by FOMODEL0:26;
hence (SubWffsOf phi) `2 is Element of (AllSymbolsOf S) * by FINSEQ_1:def 11; :: thesis: verum

end;

end;