let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for x being Point of (A . (indx b)) ex p being ManySortedSet of st
( p in product b & {(p +* (indx b),x)} = product (b +* (indx b),{x}) )
let A be PLS-yielding ManySortedSet of ; :: thesis: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for x being Point of (A . (indx b)) ex p being ManySortedSet of st
( p in product b & {(p +* (indx b),x)} = product (b +* (indx b),{x}) )
let b1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: for x being Point of (A . (indx b1)) ex p being ManySortedSet of st
( p in product b1 & {(p +* (indx b1),x)} = product (b1 +* (indx b1),{x}) )
set i = indx b1;
let x be Point of (A . (indx b1)); :: thesis: ex p being ManySortedSet of st
( p in product b1 & {(p +* (indx b1),x)} = product (b1 +* (indx b1),{x}) )
consider bb being set such that
A1: bb in product b1 by XBOOLE_0:def 1;
consider bf being Function such that
A2: ( bf = bb & dom bf = dom b1 & ( for o being set st o in dom b1 holds
bf . o in b1 . o ) ) by A1, CARD_3:def 5;
A3: ( dom b1 = I & dom (Carrier A) = I ) by PARTFUN1:def 4;
then reconsider bb = bb as ManySortedSet of by A2, PARTFUN1:def 4, RELAT_1:def 18;
take p = bb; :: thesis: ( p in product b1 & {(p +* (indx b1),x)} = product (b1 +* (indx b1),{x}) )
thus p in product b1 by A1; :: thesis: {(p +* (indx b1),x)} = product (b1 +* (indx b1),{x})
set bbx = bb +* (indx b1),x;
thus {(p +* (indx b1),x)} = product (b1 +* (indx b1),{x}) :: thesis: verum

proof

thus {(p +* (indx b1),x)} c= product (b1 +* (indx b1),{x}) :: according to XBOOLE_0:def 10 :: thesis: product (b1 +* (indx b1),{x}) c= {(p +* (indx b1),x)}

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in {(p +* (indx b1),x)} or o in product (b1 +* (indx b1),{x}) )
assume o in {(p +* (indx b1),x)} ; :: thesis: o in product (b1 +* (indx b1),{x})
then A4: o = bb +* (indx b1),x by TARSKI:def 1;
A5: dom (bb +* (indx b1),x) = I by PARTFUN1:def 4
.= dom (b1 +* (indx b1),{x}) by PARTFUN1:def 4 ;

now

let z be set ; :: thesis: ( z in dom (b1 +* (indx b1),{x}) implies (bb +* (indx b1),x) . b₁ in (b1 +* (indx b1),{x}) . b₁ )
assume z in dom (b1 +* (indx b1),{x}) ; :: thesis: (bb +* (indx b1),x) . b₁ in (b1 +* (indx b1),{x}) . b₁
then A6: z in I by PARTFUN1:def 4;
then A7: z in dom bb by PARTFUN1:def 4;

per cases ( z = indx b1 or z <> indx b1 ) ;

suppose A8: z = indx b1 ; :: thesis: (bb +* (indx b1),x) . b₁ in (b1 +* (indx b1),{x}) . b₁

then (bb +* (indx b1),x) . z = x by A7, FUNCT_7:33;
then (bb +* (indx b1),x) . z in {x} by TARSKI:def 1;
hence (bb +* (indx b1),x) . z in (b1 +* (indx b1),{x}) . z by A3, A8, FUNCT_7:33; :: thesis: verum

end;

suppose A9: z <> indx b1 ; :: thesis: (bb +* (indx b1),x) . b₁ in (b1 +* (indx b1),{x}) . b₁

then (bb +* (indx b1),x) . z = bb . z by FUNCT_7:34;
then (bb +* (indx b1),x) . z in b1 . z by A1, A3, A6, CARD_3:18;
hence (bb +* (indx b1),x) . z in (b1 +* (indx b1),{x}) . z by A9, FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence o in product (b1 +* (indx b1),{x}) by A4, A5, CARD_3:18; :: thesis: verum

end;

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in product (b1 +* (indx b1),{x}) or o in {(p +* (indx b1),x)} )
assume o in product (b1 +* (indx b1),{x}) ; :: thesis: o in {(p +* (indx b1),x)}
then consider u being Function such that
A10: ( u = o & dom u = dom (b1 +* (indx b1),{x}) & ( for z being set st z in dom (b1 +* (indx b1),{x}) holds
u . z in (b1 +* (indx b1),{x}) . z ) ) by CARD_3:def 5;
A11: dom u = I by A10, PARTFUN1:def 4
.= dom (bb +* (indx b1),x) by PARTFUN1:def 4 ;

now

let z be set ; :: thesis: ( z in dom u implies u . b₁ = (bb +* (indx b1),x) . b₁ )
assume A12: z in dom u ; :: thesis: u . b₁ = (bb +* (indx b1),x) . b₁
then A13: z in I by A10, PARTFUN1:def 4;
reconsider zz = z as Element of I by A10, A12, PARTFUN1:def 4;
A14: u . z in (b1 +* (indx b1),{x}) . z by A10, A12;

per cases ( zz = indx b1 or zz <> indx b1 ) ;

suppose A15: zz = indx b1 ; :: thesis: u . b₁ = (bb +* (indx b1),x) . b₁

then u . z in {x} by A3, A14, FUNCT_7:33;
then u . z = x by TARSKI:def 1;
hence u . z = (bb +* (indx b1),x) . z by A2, A3, A15, FUNCT_7:33; :: thesis: verum

end;

suppose A16: zz <> indx b1 ; :: thesis: u . b₁ = (bb +* (indx b1),x) . b₁

then ( not b1 . zz is empty & b1 . zz is trivial ) by PENCIL_1:def 21;
then consider o being set such that
A17: b1 . z = {o} by REALSET1:def 4;
u . z in b1 . z by A14, A16, FUNCT_7:34;
then A18: u . z = o by A17, TARSKI:def 1;
(bb +* (indx b1),x) . z = bb . z by A16, FUNCT_7:34;
then (bb +* (indx b1),x) . z in {o} by A2, A3, A13, A17;
hence u . z = (bb +* (indx b1),x) . z by A18, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then u = bb +* (indx b1),x by A11, FUNCT_1:9;
hence o in {(p +* (indx b1),x)} by A10, TARSKI:def 1; :: thesis: verum

end;