let C be initialized ConstructorSignature; :: thesis: for q being pure expression of C, a_Type C
for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)
let q be pure expression of C, a_Type C; :: thesis: for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)
let A be finite Subset of (QuasiAdjs C); :: thesis: vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)
set X = { (variables_in a) where a is quasi-adjective of C : a in A } ;
set Y = { (vars a) where a is quasi-adjective of C : a in A } ;
A1: union { (variables_in a) where a is quasi-adjective of C : a in A } c= union { (vars a) where a is quasi-adjective of C : a in A }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (variables_in a) where a is quasi-adjective of C : a in A } or x in union { (vars a) where a is quasi-adjective of C : a in A } )
assume x in union { (variables_in a) where a is quasi-adjective of C : a in A } ; :: thesis: x in union { (vars a) where a is quasi-adjective of C : a in A }
then consider Z being set such that
B0: ( x in Z & Z in { (variables_in a) where a is quasi-adjective of C : a in A } ) by TARSKI:def 4;
consider a being quasi-adjective of C such that
B1: ( Z = variables_in a & a in A ) by B0;
Z c= vars a by B1, VARCL;
then ( vars a in { (vars a) where a is quasi-adjective of C : a in A } & x in vars a ) by B0, B1;
hence x in union { (vars a) where a is quasi-adjective of C : a in A } by TARSKI:def 4; :: thesis: verum

end;

for x, y being set st [x,y] in union { (vars a) where a is quasi-adjective of C : a in A } holds
x c= union { (vars a) where a is quasi-adjective of C : a in A }

proof

let x, y be set ; :: thesis: ( [x,y] in union { (vars a) where a is quasi-adjective of C : a in A } implies x c= union { (vars a) where a is quasi-adjective of C : a in A } )
assume [x,y] in union { (vars a) where a is quasi-adjective of C : a in A } ; :: thesis: x c= union { (vars a) where a is quasi-adjective of C : a in A }
then consider Z being set such that
B2: ( [x,y] in Z & Z in { (vars a) where a is quasi-adjective of C : a in A } ) by TARSKI:def 4;
consider a being quasi-adjective of C such that
B3: ( Z = vars a & a in A ) by B2;
( x c= Z & Z c= union { (vars a) where a is quasi-adjective of C : a in A } ) by B2, B3, VARCL, ZFMISC_1:92;
hence x c= union { (vars a) where a is quasi-adjective of C : a in A } by XBOOLE_1:1; :: thesis: verum

end;

then A3: varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) c= union { (vars a) where a is quasi-adjective of C : a in A } by A1, VARCL;
A4: union { (vars a) where a is quasi-adjective of C : a in A } c= varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (vars a) where a is quasi-adjective of C : a in A } or x in varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) )
assume x in union { (vars a) where a is quasi-adjective of C : a in A } ; :: thesis: x in varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } )
then consider Z being set such that
B4: ( x in Z & Z in { (vars a) where a is quasi-adjective of C : a in A } ) by TARSKI:def 4;
consider a being quasi-adjective of C such that
B5: ( Z = vars a & a in A ) by B4;
variables_in a in { (variables_in a) where a is quasi-adjective of C : a in A } by B5;
then vars a c= varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) by Th13, ZFMISC_1:92;
hence x in varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) by B4, B5; :: thesis: verum

end;

thus vars (A ast q) = varcl ((union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)) by ThAA
.= (varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } )) \/ (vars q) by Th10
.= (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q) by A3, A4, XBOOLE_0:def 10 ; :: thesis: verum