let S be Language; :: thesis: for phi0 being 0wff string of S st (S -firstChar) . phi0 <> TheEqSymbOf S holds
phi0 is OwnSymbolsOf S -valued
let phi0 be 0wff string of S; :: thesis: ( (S -firstChar) . phi0 <> TheEqSymbOf S implies phi0 is OwnSymbolsOf S -valued )
set O = OwnSymbolsOf S;
set F = S -firstChar ;
set r = (S -firstChar) . phi0;
set C = S -multiCat ;
set sub = SubTerms phi0;
set E = TheEqSymbOf S;
set R = RelSymbolsOf S;
reconsider TS = TermSymbolsOf S as non empty Subset of (OwnSymbolsOf S) by Th1;
assume (S -firstChar) . phi0 <> TheEqSymbOf S ; :: thesis: phi0 is OwnSymbolsOf S -valued
then not (S -firstChar) . phi0 in {(TheEqSymbOf S)} by TARSKI:def 1;
then not (S -firstChar) . phi0 in (RelSymbolsOf S) \ (OwnSymbolsOf S) by Th1;
then ( (S -firstChar) . phi0 in OwnSymbolsOf S or not (S -firstChar) . phi0 in RelSymbolsOf S ) by XBOOLE_0:def 5;
then reconsider rr = (S -firstChar) . phi0 as Element of OwnSymbolsOf S by Def17;
(S -multiCat) . (SubTerms phi0) is TS -valued by FOMODEL0:54;
then reconsider tail = (S -multiCat) . (SubTerms phi0) as OwnSymbolsOf S -valued FinSequence ;
phi0 = <*rr*> ^ tail by Def38;
hence phi0 is OwnSymbolsOf S -valued ; :: thesis: verum