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 vars ((ast C) term (a,t)) = (vars a) \/ (vars t)
let t be expression of C, a_Type C; :: thesis: for a being expression of C, an_Adj C holds vars ((ast C) term (a,t)) = (vars a) \/ (vars t)
let a be expression of C, an_Adj C; :: thesis: vars ((ast C) term (a,t)) = (vars a) \/ (vars t)
thus vars ((ast C) term (a,t)) = varcl ((variables_in a) \/ (variables_in t)) by Th97
.= (vars a) \/ (vars t) by Th11 ; :: thesis: verum