let C be initialized ConstructorSignature; :: thesis: for T being quasi-type of C
for f1, f2 being valuation of C holds (T at f1) at f2 = T at (f1 at f2)
let T be quasi-type of C; :: thesis: for f1, f2 being valuation of C holds (T at f1) at f2 = T at (f1 at f2)
let f1, f2 be valuation of C; :: thesis: (T at f1) at f2 = T at (f1 at f2)
thus (T at f1) at f2 = (((adjs T) at f1) at f2) ast ((the_base_of (T at f1)) at f2)
.= ((adjs T) at (f1 at f2)) ast ((the_base_of (T at f1)) at f2) by Th150
.= ((adjs T) at (f1 at f2)) ast (((the_base_of T) at f1) at f2)
.= T at (f1 at f2) by Th149 ; :: thesis: verum