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

end;

suppose
not phi is 0wff
; :: thesis: (SubWffsOf phi) `1 is wff string of S

then consider phi1 being wff string of S, p being FinSequence such that

A1: ( p is AllSymbolsOf S -valued & SubWffsOf phi = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) by Def34;

((SubWffsOf phi) `1) \+\ phi1 = {} by A1;

hence (SubWffsOf phi) `1 is wff string of S by FOMODEL0:29; :: thesis: verum

end;A1: ( p is AllSymbolsOf S -valued & SubWffsOf phi = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) by Def34;

((SubWffsOf phi) `1) \+\ phi1 = {} by A1;

hence (SubWffsOf phi) `1 is wff string of S by FOMODEL0:29; :: thesis: verum