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 () 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 () 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 () holds f .: B is Segre-Coset of A

let B be Segre-Coset of A; :: thesis: for f being Collineation of () holds f .: B is Segre-Coset of A
consider W being Subset of () 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 () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by ;
let f be Collineation of (); :: thesis: f .: B is Segre-Coset of A
reconsider g = f " as Collineation of () by Th13;
A4: dom f = the carrier of () by FUNCT_2:def 1;
A5: dom g = the carrier of () by FUNCT_2:def 1;
A6: f is bijective by Def4;
then A7: rng f = the carrier of () by FUNCT_2:def 3;
A8: rng f = [#] () by ;
A9: f .: B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
proof
A10: W c= f " (f .: W) by ;
f " (f .: W) c= W by ;
then A11: f " (f .: W) = W by A10;
thus f .: B c= union { Y where Y is Subset of () : ( 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 () : ( 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 f .: B or o in union { Y where Y is Subset of () : ( 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 () : ( 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 () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } by ;
consider Y being Subset of () 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 ;
then A21: f .: Y in { Z where Z is Subset of () : ( not Z is trivial & Z is strong & Z is closed_under_lines & f .: W,Z are_joinable ) } by A20;
o in f .: Y by ;
hence o in union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } by ; :: thesis: verum
end;
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in union { Y where Y is Subset of () : ( 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 () : ( 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 () : ( 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 () 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 ;
( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by ;
then g .: (f .: W),g .: Y are_joinable by ;
then W,g .: Y are_joinable by ;
then A28: g .: Y in { Z where Z is Subset of () : ( not Z is trivial & Z is strong & Z is closed_under_lines & W,Z are_joinable ) } by A27;
g . o in g .: Y by ;
then A29: g . o in B by ;
o = f . ((f ") . o) by ;
then o = f . (g . o) by ;
hence o in f .: B by ; :: thesis: verum
end;
( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines ) by ;
hence f .: B is Segre-Coset of A by A1, A9, Th23; :: thesis: verum