A1: ( ( for j being Element of I holds A . j is with_non_trivial_blocks ) & ( for j being Element of I holds A . j is identifying_close_blocks ) ) ;
( not A . the Element of I is void & ( for j being Element of I holds not A . j is degenerated ) ) ;
hence ( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks ) by A1, Th15, Th16, Th17, Th18; :: thesis: verum