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 variables_in (A ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)
let q be pure expression of C, a_Type C; :: thesis: for A being finite Subset of (QuasiAdjs C) holds variables_in (A ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)
let A be finite Subset of (QuasiAdjs C); :: thesis: variables_in (A ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)
set X = ((MSVars C),(a_Term C) variables_in ) .: A;
set Y = { (variables_in a) where a is quasi-adjective of C : a in A } ;
A1: ((MSVars C),(a_Term C) variables_in ) .: A c= { (variables_in a) where a is quasi-adjective of C : a in A }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in ((MSVars C),(a_Term C) variables_in ) .: A or z in { (variables_in a) where a is quasi-adjective of C : a in A } )
assume z in ((MSVars C),(a_Term C) variables_in ) .: A ; :: thesis: z in { (variables_in a) where a is quasi-adjective of C : a in A }
then consider a being set such that
B1: ( a in dom ((MSVars C),(a_Term C) variables_in ) & a in A & z = ((MSVars C),(a_Term C) variables_in ) . a ) by FUNCT_1:def 12;
reconsider a = a as quasi-adjective of C by B1, Th52;
z = variables_in a by B1, VARS'INF;
hence z in { (variables_in a) where a is quasi-adjective of C : a in A } by B1; :: thesis: verum

end;

A2: { (variables_in a) where a is quasi-adjective of C : a in A } c= ((MSVars C),(a_Term C) variables_in ) .: A

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (variables_in a) where a is quasi-adjective of C : a in A } or z in ((MSVars C),(a_Term C) variables_in ) .: A )
assume z in { (variables_in a) where a is quasi-adjective of C : a in A } ; :: thesis: z in ((MSVars C),(a_Term C) variables_in ) .: A
then consider a being quasi-adjective of C such that
B2: ( z = variables_in a & a in A ) ;
( z = ((MSVars C),(a_Term C) variables_in ) . a & dom ((MSVars C),(a_Term C) variables_in ) = Union the Sorts of (Free C,(MSVars C)) ) by B2, VARS'INF, FUNCT_2:def 1;
hence z in ((MSVars C),(a_Term C) variables_in ) .: A by B2, FUNCT_1:def 12; :: thesis: verum

end;

thus variables_in (A ast q) = (union (((MSVars C),(a_Term C) variables_in ) .: (adjs (A ast q)))) \/ (variables_in q) by MCART_1:7
.= (union (((MSVars C),(a_Term C) variables_in ) .: A)) \/ (variables_in q) by MCART_1:7
.= (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q) by A1, A2, XBOOLE_0:def 10 ; :: thesis: verum