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 object 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 object st o in dom b1 holds

bf . o in b1 . o ) ) by A1, CARD_3:def 5;

A3: dom b1 = I by PARTFUN1:def 2;

then reconsider bb = bb as ManySortedSet of I by A2, PARTFUN1:def 2, 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

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 object 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 object st o in dom b1 holds

bf . o in b1 . o ) ) by A1, CARD_3:def 5;

A3: dom b1 = I by PARTFUN1:def 2;

then reconsider bb = bb as ManySortedSet of I by A2, PARTFUN1:def 2, 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))}

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 object st z in dom (b1 +* ((indx b1),{x})) holds

u . z in (b1 +* ((indx b1),{x})) . z by CARD_3:def 5;

.= dom (bb +* ((indx b1),x)) by PARTFUN1:def 2 ;

then u = bb +* ((indx b1),x) by A13;

hence o in {(p +* ((indx b1),x))} by A10, TARSKI:def 1; :: thesis: verum

end;proof

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 2

.= dom (b1 +* ((indx b1),{x})) by PARTFUN1:def 2 ;

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

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in product (b1 +* ((indx b1),{x})) or o in {(p +* ((indx b1),x))} )A4: now :: thesis: for z being object st z in dom (b1 +* ((indx b1),{x})) holds

(bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in {(p +* ((indx b1),x))} or o in product (b1 +* ((indx b1),{x})) )(bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z

let z be object ; :: thesis: ( z in dom (b1 +* ((indx b1),{x})) implies (bb +* ((indx b1),x)) . b_{1} in (b1 +* ((indx b1),{x})) . b_{1} )

assume z in dom (b1 +* ((indx b1),{x})) ; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (b1 +* ((indx b1),{x})) . b_{1}

then A5: z in I ;

then A6: z in dom bb by PARTFUN1:def 2;

end;assume z in dom (b1 +* ((indx b1),{x})) ; :: thesis: (bb +* ((indx b1),x)) . b

then A5: z in I ;

then A6: z in dom bb by PARTFUN1:def 2;

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

end;

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

then
(bb +* ((indx b1),x)) . z = x
by A6, FUNCT_7:31;

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:31; :: thesis: verum

end;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:31; :: thesis: verum

suppose A8:
z <> indx b1
; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (b1 +* ((indx b1),{x})) . b_{1}

then
(bb +* ((indx b1),x)) . z = bb . z
by FUNCT_7:32;

then (bb +* ((indx b1),x)) . z in b1 . z by A1, A3, A5, CARD_3:9;

hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A8, FUNCT_7:32; :: thesis: verum

end;then (bb +* ((indx b1),x)) . z in b1 . z by A1, A3, A5, CARD_3:9;

hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A8, FUNCT_7:32; :: thesis: verum

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 2

.= dom (b1 +* ((indx b1),{x})) by PARTFUN1:def 2 ;

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

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 object st z in dom (b1 +* ((indx b1),{x})) holds

u . z in (b1 +* ((indx b1),{x})) . z by CARD_3:def 5;

A13: now :: thesis: for z being object st z in dom u holds

u . z = (bb +* ((indx b1),x)) . z

dom u =
I
by A11, PARTFUN1:def 2
u . z = (bb +* ((indx b1),x)) . z

let z be object ; :: thesis: ( z in dom u implies u . b_{1} = (bb +* ((indx b1),x)) . b_{1} )

assume A14: z in dom u ; :: thesis: u . b_{1} = (bb +* ((indx b1),x)) . b_{1}

then A15: z in I by A11;

reconsider zz = z as Element of I by A11, A14;

A16: u . z in (b1 +* ((indx b1),{x})) . z by A11, A12, A14;

end;assume A14: z in dom u ; :: thesis: u . b

then A15: z in I by A11;

reconsider zz = z as Element of I by A11, A14;

A16: u . z in (b1 +* ((indx b1),{x})) . z by A11, A12, A14;

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

end;

suppose A17:
zz = indx b1
; :: thesis: u . b_{1} = (bb +* ((indx b1),x)) . b_{1}

then
u . z in {x}
by A3, A16, FUNCT_7:31;

then u . z = x by TARSKI:def 1;

hence u . z = (bb +* ((indx b1),x)) . z by A2, A3, A17, FUNCT_7:31; :: thesis: verum

end;then u . z = x by TARSKI:def 1;

hence u . z = (bb +* ((indx b1),x)) . z by A2, A3, A17, FUNCT_7:31; :: thesis: verum

suppose A18:
zz <> indx b1
; :: thesis: u . b_{1} = (bb +* ((indx b1),x)) . b_{1}

then
( not b1 . zz is empty & b1 . zz is trivial )
by PENCIL_1:def 21;

then b1 . zz is 1 -element ;

then consider o being object such that

A19: b1 . z = {o} by ZFMISC_1:131;

u . z in b1 . z by A16, A18, FUNCT_7:32;

then A20: u . z = o by A19, TARSKI:def 1;

(bb +* ((indx b1),x)) . z = bb . z by A18, FUNCT_7:32;

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;then b1 . zz is 1 -element ;

then consider o being object such that

A19: b1 . z = {o} by ZFMISC_1:131;

u . z in b1 . z by A16, A18, FUNCT_7:32;

then A20: u . z = o by A19, TARSKI:def 1;

(bb +* ((indx b1),x)) . z = bb . z by A18, FUNCT_7:32;

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

.= dom (bb +* ((indx b1),x)) by PARTFUN1:def 2 ;

then u = bb +* ((indx b1),x) by A13;

hence o in {(p +* ((indx b1),x))} by A10, TARSKI:def 1; :: thesis: verum