let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I 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 I; :: 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

consider W being Subset of (Segre_Product A) such that

A2: ( not W is trivial & W is strong & W is closed_under_lines ) and

A3: 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;

let f be Collineation of (Segre_Product A); :: thesis: f .: B is Segre-Coset of A

reconsider g = f " as Collineation of (Segre_Product A) by Th13;

A4: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

A5: dom g = the carrier of (Segre_Product A) by FUNCT_2:def 1;

A6: f is bijective by Def4;

then A7: rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;

A8: rng f = [#] (Segre_Product A) by A6, FUNCT_2:def 3;

A9: 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 ) }

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

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 I; :: 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

consider W being Subset of (Segre_Product A) such that

A2: ( not W is trivial & W is strong & W is closed_under_lines ) and

A3: 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;

let f be Collineation of (Segre_Product A); :: thesis: f .: B is Segre-Coset of A

reconsider g = f " as Collineation of (Segre_Product A) by Th13;

A4: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

A5: dom g = the carrier of (Segre_Product A) by FUNCT_2:def 1;

A6: f is bijective by Def4;

then A7: rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;

A8: rng f = [#] (Segre_Product A) by A6, FUNCT_2:def 3;

A9: 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

( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines )
by A2, Th14, Th16, Th18;
A10:
W c= f " (f .: W)
by A4, FUNCT_1:76;

f " (f .: W) c= W by A6, FUNCT_1:82;

then A11: f " (f .: W) = W by A10;

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

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

A22: o in u and

A23: 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

A24: u = Y and

A25: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and

A26: f .: W,Y are_joinable by A23;

A27: ( not g .: Y is trivial & g .: Y is strong & g .: Y is closed_under_lines ) by A25, Th14, Th16, Th18;

( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A2, Th14, Th16, Th18;

then g .: (f .: W),g .: Y are_joinable by A25, A26, Th20;

then W,g .: Y are_joinable by A6, A8, A11, TOPS_2:55;

then A28: 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 A27;

g . o in g .: Y by A5, A22, A24, FUNCT_1:def 6;

then A29: g . o in B by A3, A28, TARSKI:def 4;

o = f . ((f ") . o) by A6, A7, A22, A24, FUNCT_1:35;

then o = f . (g . o) by A6, TOPS_2:def 4;

hence o in f .: B by A4, A29, FUNCT_1:def 6; :: thesis: verum

end;f " (f .: W) c= W by A6, FUNCT_1:82;

then A11: f " (f .: W) = W by A10;

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 object ; :: 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 )
let o be object ; :: 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 object such that

A12: u in dom f and

A13: u in B and

A14: o = f . u by FUNCT_1:def 6;

consider y being set such that

A15: u in y and

A16: 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 A3, A13, TARSKI:def 4;

consider Y being Subset of (Segre_Product A) such that

A17: y = Y and

A18: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and

A19: W,Y are_joinable by A16;

A20: f .: W,f .: Y are_joinable by A2, A18, A19, Th20;

( not f .: Y is trivial & f .: Y is strong & f .: Y is closed_under_lines ) by A18, Th14, Th16, Th18;

then A21: 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 A20;

o in f .: Y by A12, A14, A15, A17, FUNCT_1:def 6;

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 A21, TARSKI:def 4; :: thesis: verum

end;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 object such that

A12: u in dom f and

A13: u in B and

A14: o = f . u by FUNCT_1:def 6;

consider y being set such that

A15: u in y and

A16: 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 A3, A13, TARSKI:def 4;

consider Y being Subset of (Segre_Product A) such that

A17: y = Y and

A18: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and

A19: W,Y are_joinable by A16;

A20: f .: W,f .: Y are_joinable by A2, A18, A19, Th20;

( not f .: Y is trivial & f .: Y is strong & f .: Y is closed_under_lines ) by A18, Th14, Th16, Th18;

then A21: 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 A20;

o in f .: Y by A12, A14, A15, A17, FUNCT_1:def 6;

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 A21, TARSKI:def 4; :: thesis: verum

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

A22: o in u and

A23: 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

A24: u = Y and

A25: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and

A26: f .: W,Y are_joinable by A23;

A27: ( not g .: Y is trivial & g .: Y is strong & g .: Y is closed_under_lines ) by A25, Th14, Th16, Th18;

( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by A2, Th14, Th16, Th18;

then g .: (f .: W),g .: Y are_joinable by A25, A26, Th20;

then W,g .: Y are_joinable by A6, A8, A11, TOPS_2:55;

then A28: 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 A27;

g . o in g .: Y by A5, A22, A24, FUNCT_1:def 6;

then A29: g . o in B by A3, A28, TARSKI:def 4;

o = f . ((f ") . o) by A6, A7, A22, A24, FUNCT_1:35;

then o = f . (g . o) by A6, TOPS_2:def 4;

hence o in f .: B by A4, A29, FUNCT_1:def 6; :: thesis: verum

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