per cases ( not phi is 0wff or phi is 0wff ) ;
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;
suppose phi is 0wff ; :: thesis: (SubWffsOf phi) `1 is wff string of S
then SubWffsOf phi = [phi,{}] by Def34;
then ((SubWffsOf phi) `1) \+\ phi = {} ;
hence (SubWffsOf phi) `1 is wff string of S by FOMODEL0:29; :: thesis: verum
end;
end;