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
A2: ( p is AllSymbolsOf S -valued & SubWffsOf phi = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) by Def34;
( (SubWffsOf phi) `2 = p & p is FinSequence of AllSymbolsOf S ) by A2, FOMODEL0:26;
hence (SubWffsOf phi) `2 is Element of (AllSymbolsOf S) * ; :: thesis: verum

end;

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

then SubWffsOf phi = [phi,{}] by Def34;
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) * ; :: thesis: verum

end;

end;