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 Th46;
then variables_in ((ast C) term (a,t)) = ((C variables_in a) (\/) (C variables_in t)) . a_Term by Th96;
hence variables_in ((ast C) term (a,t)) = (variables_in a) \/ (variables_in t) by PBOOLE:def 4; :: thesis: verum