let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I
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 I st
( p in product b & {(p +* (indx b),x)} = product (b +* (indx b),{x}) )
let A be PLS-yielding ManySortedSet of I; :: 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 I 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 I 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 I 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;
A2: ex bf being Function st
( 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 by PARTFUN1:def 4;
then reconsider bb = bb as ManySortedSet of I 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

A4: 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 A5: z in I by PARTFUN1:def 4;
then A6: z in dom bb by PARTFUN1:def 4;

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

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

then (bb +* (indx b1),x) . z = x by A6, 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, A7, FUNCT_7:33; :: thesis: verum

end;

suppose A8: 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, A5, CARD_3:18;
hence (bb +* (indx b1),x) . z in (b1 +* (indx b1),{x}) . z by A8, FUNCT_7:34; :: thesis: verum

end;

end;

end;

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 A9: o = bb +* (indx b1),x by TARSKI:def 1;
dom (bb +* (indx b1),x) = I by PARTFUN1:def 4
.= dom (b1 +* (indx b1),{x}) by PARTFUN1:def 4 ;
hence o in product (b1 +* (indx b1),{x}) by A9, A4, 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 and
A11: dom u = dom (b1 +* (indx b1),{x}) and
A12: 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;

A13: now

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

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

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

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

end;

suppose A18: 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
A19: b1 . z = {o} by REALSET1:def 4;
u . z in b1 . z by A16, A18, FUNCT_7:34;
then A20: u . z = o by A19, TARSKI:def 1;
(bb +* (indx b1),x) . z = bb . z by A18, FUNCT_7:34;
then (bb +* (indx b1),x) . z in {o} by A2, A3, A15, A19;
hence u . z = (bb +* (indx b1),x) . z by A20, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;