let I be non empty set ; :: thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds
not Segre_Product A is degenerated
let A be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) implies not Segre_Product A is degenerated )
assume A1: for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ; :: thesis: not Segre_Product A is degenerated
then not Segre_Product A is void by Th15;
then reconsider SB = Segre_Blocks A as non empty set ;
now :: thesis: not product (Carrier A) in SB
assume product (Carrier A) in SB ; :: thesis: contradiction
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: product (Carrier A) = product B and
A3: ex i being Element of I st B . i is Block of (A . i) by Def22;
consider i being Element of I such that
A4: B . i is Block of (A . i) by A3;
B is V2() by A2, Th1;
then ( ex R being 1-sorted st
( R = A . i & the carrier of R = (Carrier A) . i ) & (Carrier A) . i is Block of (A . i) ) by A2, A4, PRALG_1:def 15, PUA2MSS1:2;
then A . i is degenerated ;
hence contradiction by A1; :: thesis: verum
end;
then product (Carrier A) is not Element of SB ;
hence not Segre_Product A is degenerated ; :: thesis: verum