let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
let A be PLS-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A )
assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
let B be Segre-Coset of A; :: thesis: for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
let f be Collineation of (Segre_Product A); :: thesis: f .: B is Segre-Coset of A
f is bijective by Def4;
then A2: ( f is one-to-one & f is onto ) ;
then A3: rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;
A4: rng f = [#] (Segre_Product A) by A2, FUNCT_2:def 3;
reconsider g = f " as Collineation of (Segre_Product A) by Th13;
A5: ( dom f = the carrier of (Segre_Product A) & dom g = the carrier of (Segre_Product A) ) by FUNCT_2:def 1;
consider W being Subset of (Segre_Product A) such that
A6: ( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) by A1, Th23;
A7: ( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A6, Th14, Th16, Th18;
f .: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }

proof

thus f .: B c= union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } :: according to XBOOLE_0:def 10 :: thesis: union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } c= f .: B

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in f .: B or o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } )
assume o in f .: B ; :: thesis: o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
then consider u being set such that
A8: ( u in dom f & u in B & o = f . u ) by FUNCT_1:def 12;
consider y being set such that
A9: ( u in y & y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) by A6, A8, TARSKI:def 4;
consider Y being Subset of (Segre_Product A) such that
A10: ( y = Y & not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) by A9;
A11: ( not f .: Y is trivial & f .: Y is strong & f .: Y is closed_under_lines ) by A10, Th14, Th16, Th18;
f .: W,f .: Y are_joinable by A6, A10, Th20;
then A12: f .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & f .: W,Z are_joinable ) } by A11;
o in f .: Y by A8, A9, A10, FUNCT_1:def 12;
hence o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } by A12, TARSKI:def 4; :: thesis: verum

end;

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } or o in f .: B )
assume o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } ; :: thesis: o in f .: B
then consider u being set such that
A13: ( o in u & u in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } ) by TARSKI:def 4;
consider Y being Subset of (Segre_Product A) such that
A14: ( u = Y & not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) by A13;
( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A6, Th14, Th16, Th18;
then A15: g .: (f .: W),g .: Y are_joinable by A14, Th20;
A16: f " (f .: W) c= W by A2, FUNCT_1:152;
W c= f " (f .: W) by A5, FUNCT_1:146;
then f " (f .: W) = W by A16, XBOOLE_0:def 10;
then A17: W,g .: Y are_joinable by A2, A4, A15, TOPS_2:68;
( not g .: Y is trivial & g .: Y is strong & g .: Y is closed_under_lines ) by A14, Th14, Th16, Th18;
then A18: g .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & W,Z are_joinable ) } by A17;
g . o in g .: Y by A5, A13, A14, FUNCT_1:def 12;
then A19: g . o in B by A6, A18, TARSKI:def 4;
o = f . ((f " ) . o) by A2, A3, A13, A14, FUNCT_1:57;
then o = f . (g . o) by A2, A3, TOPS_2:def 4;
hence o in f .: B by A5, A19, FUNCT_1:def 12; :: thesis: verum

end;

hence f .: B is Segre-Coset of A by A1, A7, Th23; :: thesis: verum