let C be initialized ConstructorSignature; :: thesis: for T being quasi-type of C
for a being quasi-adjective of C holds variables_in (a ast T) = (variables_in a) \/ (variables_in T)
let T be quasi-type of C; :: thesis: for a being quasi-adjective of C holds variables_in (a ast T) = (variables_in a) \/ (variables_in T)
let a be quasi-adjective of C; :: thesis: variables_in (a ast T) = (variables_in a) \/ (variables_in T)
A1: dom ((MSVars C),(a_Term C) variables_in ) = Union the Sorts of (Free C,(MSVars C)) by FUNCT_2:def 1;
thus variables_in (a ast T) = (union (((MSVars C),(a_Term C) variables_in ) .: (adjs (a ast T)))) \/ (variables_in (the_base_of T)) by MCART_1:7
.= (union (((MSVars C),(a_Term C) variables_in ) .: ({a} \/ (adjs T)))) \/ (variables_in (the_base_of T)) by MCART_1:7
.= (union ((((MSVars C),(a_Term C) variables_in ) .: {a}) \/ (((MSVars C),(a_Term C) variables_in ) .: (adjs T)))) \/ (variables_in (the_base_of T)) by RELAT_1:153
.= ((union (((MSVars C),(a_Term C) variables_in ) .: {a})) \/ (union (((MSVars C),(a_Term C) variables_in ) .: (adjs T)))) \/ (variables_in (the_base_of T)) by ZFMISC_1:96
.= (union (Im ((MSVars C),(a_Term C) variables_in ),a)) \/ (variables_in T) by XBOOLE_1:4
.= (union {(((MSVars C),(a_Term C) variables_in ) . a)}) \/ (variables_in T) by A1, FUNCT_1:117
.= (((MSVars C),(a_Term C) variables_in ) . a) \/ (variables_in T) by ZFMISC_1:31
.= (variables_in a) \/ (variables_in T) by VARS'INF ; :: thesis: verum