let C be initialized ConstructorSignature; :: thesis: for t being expression of C, a_Type C
for a being expression of C, an_Adj C holds variables_in ((ast C) term a,t) = (variables_in a) \/ (variables_in t)
let t be expression of C, a_Type C; :: thesis: for a being expression of C, an_Adj C holds variables_in ((ast C) term a,t) = (variables_in a) \/ (variables_in t)
let a be expression of C, an_Adj C; :: thesis: variables_in ((ast C) term a,t) = (variables_in a) \/ (variables_in t)
(ast C) term a,t = [* ,the carrier of C] -tree <*a,t*> by ThAst;
then variables_in ((ast C) term a,t) = ((C variables_in a) \/ (C variables_in t)) . a_Term by Aux2;
hence variables_in ((ast C) term a,t) = (variables_in a) \/ (variables_in t) by PBOOLE:def 7; :: thesis: verum