let A, B be functional set ; :: thesis: SymbolsOf (A \/ B) = (SymbolsOf A) \/ (SymbolsOf B)
set AF = { (rng x) where x is Element of A : x in A } ;
set BF = { (rng x) where x is Element of B : x in B } ;
set F = { (rng x) where x is Element of A \/ B : x in A \/ B } ;
( A null B c= A \/ B & B null A c= A \/ B ) ;
then reconsider AFF = { (rng x) where x is Element of A : x in A } , BFF = { (rng x) where x is Element of B : x in B } as Subset of { (rng x) where x is Element of A \/ B : x in A \/ B } by Lm51;
A1: AFF \/ BFF c= { (rng x) where x is Element of A \/ B : x in A \/ B } ;

now :: thesis: for y being object st y in { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } holds
y in { (rng x) where x is Element of A : x in A }

let y be object ; :: thesis: ( y in { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } implies y in { (rng x) where x is Element of A : x in A } )
assume y in { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } ; :: thesis: y in { (rng x) where x is Element of A : x in A }
then A2: ( y in { (rng x) where x is Element of A \/ B : x in A \/ B } & not y in { (rng x) where x is Element of B : x in B } ) by XBOOLE_0:def 5;
then consider x being Element of A \/ B such that
A3: ( y = rng x & x in A \/ B ) ;
not x in B by A3, A2;
then A4: x in A null {{}} by A3, XBOOLE_0:def 3;
then reconsider xx = x as Element of A \/ {{}} ;
thus y in { (rng x) where x is Element of A : x in A } by A4, A3; :: thesis: verum

end;

then ( { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } ) \/ { (rng x) where x is Element of B : x in B } c= { (rng x) where x is Element of A : x in A } \/ { (rng x) where x is Element of B : x in B } by XBOOLE_1:9, TARSKI:def 3;
then { (rng x) where x is Element of A \/ B : x in A \/ B } null BFF c= { (rng x) where x is Element of A : x in A } \/ { (rng x) where x is Element of B : x in B } by XBOOLE_1:39;
then A5: { (rng x) where x is Element of A : x in A } \/ { (rng x) where x is Element of B : x in B } = { (rng x) where x is Element of A \/ B : x in A \/ B } by A1;
thus SymbolsOf (A \/ B) = (SymbolsOf A) \/ (SymbolsOf B) by A5, ZFMISC_1:78; :: thesis: verum