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 object ; :: 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 object 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 6;
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 object ; :: 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 6; :: thesis: verum
end;
thus variables_in (A ast q) = (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs (A ast q)))) \/ (variables_in q)
.= (union ((((MSVars C),(a_Term C)) variables_in) .: A)) \/ (variables_in q)
.= (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