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

end;

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;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

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;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