let C be initialized ConstructorSignature; :: thesis: for T being quasi-type of C holds T = (adjs T) ast (the_base_of T)
let T be quasi-type of C; :: thesis: T = (adjs T) ast (the_base_of T)
thus T = (adjs T) ast (the_base_of T) ; :: thesis: verum