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
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;
A2: f is bijective by Def4;
then rng f = [#] (Segre_Product A) by FUNCT_2:def 3;
then f " B = g .: B by A2, TOPS_2:55;
hence f " B is Segre-Coset of A by A1, Th24; :: thesis: verum