set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
reconsider DA = (((AllSymbolsOf S) *) \ {{}}) /\ A, DF = (((AllSymbolsOf S) *) \ {{}}) /\ F as Subset of (((AllSymbolsOf S) *) \ {{}}) ;
reconsider D = DA \/ DF as Subset of (((AllSymbolsOf S) *) \ {{}}) ;
A1: D = (((AllSymbolsOf S) *) \ {{}}) /\ (A \/ F) by XBOOLE_1:23;
let s be F -absent Element of S; :: thesis: ( s is A -absent implies s is A \/ F -absent )
assume s is A -absent ; :: thesis: s is A \/ F -absent
then ( not s in SymbolsOf DA & not s in SymbolsOf DF ) by Def37;
then not s in (SymbolsOf DA) \/ (SymbolsOf DF) by XBOOLE_0:def 3;
then not s in SymbolsOf D by FOMODEL0:47;
hence s is A \/ F -absent by A1; :: thesis: verum