let C be initialized ConstructorSignature; :: thesis: for f being valuation of C
for T being quasi-type of C
for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f)
let f be valuation of C; :: thesis: for T being quasi-type of C
for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f)
let T be quasi-type of C; :: thesis: for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f)
let a be quasi-adjective of C; :: thesis: (a ast T) at f = (a at f) ast (T at f)
a in QuasiAdjs C ;
then reconsider A = {a} as Subset of (QuasiAdjs C) by ZFMISC_1:31;
thus (a ast T) at f = [((adjs (a ast T)) at f),((the_base_of T) at f)]
.= [((A \/ (adjs T)) at f),((the_base_of T) at f)]
.= [((A at f) \/ ((adjs T) at f)),((the_base_of T) at f)] by Th145
.= [({(a at f)} \/ ((adjs T) at f)),((the_base_of T) at f)] by Th144
.= [({(a at f)} \/ (adjs (T at f))),((the_base_of T) at f)]
.= (a at f) ast (T at f) ; :: thesis: verum