consider i being Element of I;
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 . i is void & ( for j being Element of I holds not A . j is degenerated ) ) ;
hence Segre_Product A is PLS by A1, Th15, Th16, Th17, Th18; :: thesis: verum