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
a in dom ((MSVars C),(a_Term C) variables_in ) and
A2: a in A and
A3: z = ((MSVars C),(a_Term C) variables_in ) . a by FUNCT_1:def 12;
reconsider a = a as quasi-adjective of C by A2, Th63;
z = variables_in a by A3, Def45;
hence z in { (variables_in a) where a is quasi-adjective of C : a in A } by A2; :: thesis: verum

end;

A4: { (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
A5: z = variables_in a and
A6: a in A ;
A7: z = ((MSVars C),(a_Term C) variables_in ) . a by A5, Def45;
dom ((MSVars C),(a_Term C) variables_in ) = Union the Sorts of (Free C,(MSVars C)) by FUNCT_2:def 1;
hence z in ((MSVars C),(a_Term C) variables_in ) .: A by A6, A7, 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, A4, XBOOLE_0:def 10 ; :: thesis: verum