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

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