let I be non empty set ; :: thesis: for A being ManySortedSet of I
for i, S being set holds {A} +* i,S is Segre-like
let A be ManySortedSet of I; :: thesis: for i, S being set holds {A} +* i,S is Segre-like
let i, S be set ; :: thesis: {A} +* i,S is Segre-like

per cases ( not i in I or i in I ) ;

suppose not i in I ; :: thesis: {A} +* i,S is Segre-like

then not i in dom {A} by PARTFUN1:def 4;
hence {A} +* i,S is Segre-like by FUNCT_7:def 3; :: thesis: verum

end;

suppose i in I ; :: thesis: {A} +* i,S is Segre-like

then reconsider i = i as Element of I ;
take i ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st i <> j holds
( not ({A} +* i,S) . j is empty & ({A} +* i,S) . j is trivial )
let j be Element of I; :: thesis: ( i <> j implies ( not ({A} +* i,S) . j is empty & ({A} +* i,S) . j is trivial ) )
assume A1: i <> j ; :: thesis: ( not ({A} +* i,S) . j is empty & ({A} +* i,S) . j is trivial )
{A} . j = {(A . j)} by PZFMISC1:def 1;
hence ( not ({A} +* i,S) . j is empty & ({A} +* i,S) . j is trivial ) by A1, FUNCT_7:34; :: thesis: verum

end;

end;