let C be initialized ConstructorSignature; 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; 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; 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))
.=
(union ((((MSVars C),(a_Term C)) variables_in) .: ({a} \/ (adjs T)))) \/ (variables_in (the_base_of T))
.=
(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:120
.=
((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:78
.=
(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:59
.=
((((MSVars C),(a_Term C)) variables_in) . a) \/ (variables_in T)
by ZFMISC_1:25
.=
(variables_in a) \/ (variables_in T)
by Def45
; verum