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)
ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st T = [A,q] by Th72;
hence T = (adjs T) ast (the_base_of T) by MCART_1:8; :: thesis: verum