let C be initialized ConstructorSignature; :: thesis: for T1, T2 being quasi-type of C st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 holds
T1 = T2
let T1, T2 be quasi-type of C; :: thesis: ( adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 implies T1 = T2 )
T1 = (adjs T1) ast (the_base_of T1) ;
hence ( adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 implies T1 = T2 ) by Th80; :: thesis: verum