let C be initialized ConstructorSignature; :: thesis: for T being quasi-type of C
for a being quasi-adjective of C holds vars (a ast T) = (vars a) \/ (vars T)
let T be quasi-type of C; :: thesis: for a being quasi-adjective of C holds vars (a ast T) = (vars a) \/ (vars T)
let a be quasi-adjective of C; :: thesis: vars (a ast T) = (vars a) \/ (vars T)
thus vars (a ast T) = varcl ((variables_in a) \/ (variables_in T)) by Th102
.= (vars a) \/ (vars T) by Th11 ; :: thesis: verum