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
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 :: 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 z be object ; :: thesis: ( z in dom (b1 +* ((indx b1),{x})) implies (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 )
assume z in dom (b1 +* ((indx b1),{x})) ; :: thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
then A5: z in I ;
then A6: z in dom bb by PARTFUN1:def 2;
per cases ( z = indx b1 or z <> indx b1 ) ;
suppose A7: z = indx b1 ; :: thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
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;
suppose A8: z <> indx b1 ; :: thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
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;
end;
end;
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})) )
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))} )
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
let z be object ; :: thesis: ( z in dom u implies u . b1 = (bb +* ((indx b1),x)) . b1 )
assume A14: z in dom u ; :: thesis: u . b1 = (bb +* ((indx b1),x)) . b1
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 ) ;
suppose A17: zz = indx b1 ; :: thesis: u . b1 = (bb +* ((indx b1),x)) . b1
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;
suppose A18: zz <> indx b1 ; :: thesis: u . b1 = (bb +* ((indx b1),x)) . b1
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;
end;
end;
dom u = I by A11, PARTFUN1:def 2
.= 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;