let A be partial non-empty UAStr ; for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A)
set P = Class (LimDomRel A);
let f be operation of A; f is_exactly_partitable_wrt Class (LimDomRel A)
hereby PUA2MSS1:def 8,
PUA2MSS1:def 9 for p being FinSequence of Class (LimDomRel A) st product p meets dom f holds
product p c= dom f
let p be
FinSequence of
Class (LimDomRel A);
ex a being Element of Class (LimDomRel A) st f .: (product a) c= b2set a0 = the
Element of
Class (LimDomRel A);
per cases
( product p meets dom f or product p misses dom f )
;
suppose
product p meets dom f
;
ex a being Element of Class (LimDomRel A) st f .: (product a) c= b2then consider x being
object such that A1:
x in product p
and A2:
x in dom f
by XBOOLE_0:3;
f . x in the
carrier of
A
by A2, PARTFUN1:4;
then reconsider a =
Class (
(LimDomRel A),
(f . x)) as
Element of
Class (LimDomRel A) by EQREL_1:def 3;
take a =
a;
f .: (product p) c= athus
f .: (product p) c= a
verumproof
let y be
object ;
TARSKI:def 3 ( not y in f .: (product p) or y in a )
assume
y in f .: (product p)
;
y in a
then consider z being
object such that
z in dom f
and A3:
z in product p
and A4:
y = f . z
by FUNCT_1:def 6;
A5:
product p c= Funcs (
(dom p),
(Union p))
by FUNCT_6:1;
then A6:
ex
f being
Function st
(
x = f &
dom f = dom p &
rng f c= Union p )
by A1, FUNCT_2:def 2;
A7:
ex
f being
Function st
(
z = f &
dom f = dom p &
rng f c= Union p )
by A3, A5, FUNCT_2:def 2;
reconsider x =
x,
z =
z as
Function by A1, A3;
A8:
dom p = Seg (len p)
by FINSEQ_1:def 3;
then reconsider x =
x,
z =
z as
FinSequence by A6, A7, FINSEQ_1:def 2;
defpred S1[
set ]
means ( $1
in dom f &
f . $1
in a );
defpred S2[
set ,
set ]
means [$1,$2] in LimDomRel A;
len x = len p
by A6, A8, FINSEQ_1:def 3;
then A9:
len x = len z
by A7, A8, FINSEQ_1:def 3;
A10:
S1[
x]
by A2, EQREL_1:20, PARTFUN1:4;
A11:
for
p1,
q1 being
FinSequence for
z1,
z2 being
set st
S1[
(p1 ^ <*z1*>) ^ q1] &
S2[
z1,
z2] holds
S1[
(p1 ^ <*z2*>) ^ q1]
proof
let p1,
q1 be
FinSequence;
for z1, z2 being set st S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] holds
S1[(p1 ^ <*z2*>) ^ q1]let z1,
z2 be
set ;
( S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] implies S1[(p1 ^ <*z2*>) ^ q1] )
assume that A12:
(p1 ^ <*z1*>) ^ q1 in dom f
and A13:
f . ((p1 ^ <*z1*>) ^ q1) in a
and A14:
[z1,z2] in LimDomRel A
;
S1[(p1 ^ <*z2*>) ^ q1]
A15:
[(f . ((p1 ^ <*z1*>) ^ q1)),(f . x)] in LimDomRel A
by A13, EQREL_1:19;
A16:
LimDomRel A c= DomRel A
by Th21;
A17:
z1 in the
carrier of
A
by A14, ZFMISC_1:87;
A18:
z2 in the
carrier of
A
by A14, ZFMISC_1:87;
hence A19:
(p1 ^ <*z2*>) ^ q1 in dom f
by A12, A14, A16, A17, Def4;
f . ((p1 ^ <*z2*>) ^ q1) in a
A20:
f . ((p1 ^ <*z1*>) ^ q1) in rng f
by A12, FUNCT_1:def 3;
A21:
f . ((p1 ^ <*z2*>) ^ q1) in rng f
by A19, FUNCT_1:def 3;
now for i being Element of NAT holds [(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in (DomRel A) |^ (A,i)let i be
Element of
NAT ;
[(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in (DomRel A) |^ (A,i)
[z1,z2] in (DomRel A) |^ (
A,
(i + 1))
by A14, A17, A18, Def7;
then
[z1,z2] in ((DomRel A) |^ (A,i)) |^ A
by Th16;
then A22:
[(f . ((p1 ^ <*z1*>) ^ q1)),(f . ((p1 ^ <*z2*>) ^ q1))] in (DomRel A) |^ (
A,
i)
by A12, A17, A18, A19, Def5;
(
(DomRel A) |^ (
A,
i) is
total &
(DomRel A) |^ (
A,
i) is
symmetric &
(DomRel A) |^ (
A,
i) is
transitive )
by Th20;
hence
[(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in (DomRel A) |^ (
A,
i)
by A22, EQREL_1:6;
verum end;
then
[(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in LimDomRel A
by A20, A21, Def7;
then
[(f . ((p1 ^ <*z2*>) ^ q1)),(f . x)] in LimDomRel A
by A15, EQREL_1:7;
hence
f . ((p1 ^ <*z2*>) ^ q1) in a
by EQREL_1:19;
verum
end;
A23:
for
i being
Element of
NAT st
i in dom x holds
S2[
x . i,
z . i]
proof
let i be
Element of
NAT ;
( i in dom x implies S2[x . i,z . i] )
assume A24:
i in dom x
;
S2[x . i,z . i]
then
p . i in rng p
by A6, FUNCT_1:def 3;
then reconsider a =
p . i as
Element of
Class (LimDomRel A) ;
A25:
ex
g being
Function st
(
x = g &
dom g = dom p & ( for
x being
object st
x in dom p holds
g . x in p . x ) )
by A1, CARD_3:def 5;
A26:
ex
g being
Function st
(
z = g &
dom g = dom p & ( for
x being
object st
x in dom p holds
g . x in p . x ) )
by A3, CARD_3:def 5;
A27:
ex
b being
object st
(
b in the
carrier of
A &
a = Class (
(LimDomRel A),
b) )
by EQREL_1:def 3;
A28:
x . i in a
by A24, A25;
z . i in a
by A24, A25, A26;
hence
S2[
x . i,
z . i]
by A27, A28, EQREL_1:22;
verum
end;
S1[
z]
from PUA2MSS1:sch 4(A10, A9, A11, A23);
hence
y in a
by A4;
verum
end; end;
end;
let p be FinSequence of Class (LimDomRel A); ( product p meets dom f implies product p c= dom f )
assume
product p meets dom f
; product p c= dom f
then consider x being object such that
A29:
x in product p
and
A30:
x in dom f
by XBOOLE_0:3;
let y be object ; TARSKI:def 3 ( not y in product p or y in dom f )
assume A31:
y in product p
; y in dom f
A32:
product p c= Funcs ((dom p),(Union p))
by FUNCT_6:1;
then A33:
ex f being Function st
( x = f & dom f = dom p & rng f c= Union p )
by A29, FUNCT_2:def 2;
A34:
ex f being Function st
( y = f & dom f = dom p & rng f c= Union p )
by A31, A32, FUNCT_2:def 2;
reconsider x = x, z = y as Function by A29, A31;
A35:
dom p = Seg (len p)
by FINSEQ_1:def 3;
then reconsider x = x, z = z as FinSequence by A33, A34, FINSEQ_1:def 2;
defpred S1[ set ] means $1 in dom f;
defpred S2[ set , set ] means [$1,$2] in LimDomRel A;
len x = len p
by A33, A35, FINSEQ_1:def 3;
then A36:
len x = len z
by A34, A35, FINSEQ_1:def 3;
A37:
S1[x]
by A30;
A38:
for p1, q1 being FinSequence
for z1, z2 being set st S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] holds
S1[(p1 ^ <*z2*>) ^ q1]
proof
let p1,
q1 be
FinSequence;
for z1, z2 being set st S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] holds
S1[(p1 ^ <*z2*>) ^ q1]let z1,
z2 be
set ;
( S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] implies S1[(p1 ^ <*z2*>) ^ q1] )
assume that A39:
(p1 ^ <*z1*>) ^ q1 in dom f
and A40:
[z1,z2] in LimDomRel A
;
S1[(p1 ^ <*z2*>) ^ q1]
A41:
LimDomRel A c= DomRel A
by Th21;
A42:
z1 in the
carrier of
A
by A40, ZFMISC_1:87;
z2 in the
carrier of
A
by A40, ZFMISC_1:87;
hence
S1[
(p1 ^ <*z2*>) ^ q1]
by A39, A40, A41, A42, Def4;
verum
end;
A43:
for i being Element of NAT st i in dom x holds
S2[x . i,z . i]
proof
let i be
Element of
NAT ;
( i in dom x implies S2[x . i,z . i] )
assume A44:
i in dom x
;
S2[x . i,z . i]
then
p . i in rng p
by A33, FUNCT_1:def 3;
then reconsider a =
p . i as
Element of
Class (LimDomRel A) ;
A45:
ex
g being
Function st
(
x = g &
dom g = dom p & ( for
x being
object st
x in dom p holds
g . x in p . x ) )
by A29, CARD_3:def 5;
A46:
ex
g being
Function st
(
z = g &
dom g = dom p & ( for
x being
object st
x in dom p holds
g . x in p . x ) )
by A31, CARD_3:def 5;
A47:
ex
b being
object st
(
b in the
carrier of
A &
a = Class (
(LimDomRel A),
b) )
by EQREL_1:def 3;
A48:
x . i in a
by A44, A45;
z . i in a
by A44, A45, A46;
hence
S2[
x . i,
z . i]
by A47, A48, EQREL_1:22;
verum
end;
S1[z]
from PUA2MSS1:sch 4(A37, A36, A38, A43);
hence
y in dom f
; verum