let A be partial non-empty UAStr ; :: thesis: 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; :: thesis: f is_exactly_partitable_wrt Class (LimDomRel A)

hereby :: according to PUA2MSS1:def 8,PUA2MSS1:def 9 :: thesis: 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); :: thesis: ex a being Element of Class (LimDomRel A) st f .: (product a) c= b₂
set 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 ; :: thesis: ex a being Element of Class (LimDomRel A) st f .: (product a) c= b₂

then 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; :: thesis: f .: (product p) c= a
thus f .: (product p) c= a :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (product p) or y in a )
assume y in f .: (product p) ; :: thesis: 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 S₁[ set ] means ( $1 in dom f & f . $1 in a );
defpred S₂[ 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: S₁[x] by A2, EQREL_1:20, PARTFUN1:4;
A11: for p1, q1 being FinSequence
for z1, z2 being set st S₁[(p1 ^ <*z1*>) ^ q1] & S₂[z1,z2] holds
S₁[(p1 ^ <*z2*>) ^ q1]

proof

let p1, q1 be FinSequence; :: thesis: for z1, z2 being set st S₁[(p1 ^ <*z1*>) ^ q1] & S₂[z1,z2] holds
S₁[(p1 ^ <*z2*>) ^ q1]
let z1, z2 be set ; :: thesis: ( S₁[(p1 ^ <*z1*>) ^ q1] & S₂[z1,z2] implies S₁[(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 ; :: thesis: S₁[(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; :: thesis: 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 :: thesis: 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 ; :: thesis: [(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; :: thesis: 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; :: thesis: verum

end;

A23: for i being Element of NAT st i in dom x holds
S₂[x . i,z . i]

proof

let i be Element of NAT ; :: thesis: ( i in dom x implies S₂[x . i,z . i] )
assume A24: i in dom x ; :: thesis: S₂[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 S₂[x . i,z . i] by A27, A28, EQREL_1:22; :: thesis: verum

end;

S₁[z] from PUA2MSS1:sch 4(A10, A9, A11, A23);
hence y in a by A4; :: thesis: verum

end;

end;

suppose product p misses dom f ; :: thesis: ex a being Element of Class (LimDomRel A) st f .: (product a) c= b₂

then (product p) /\ (dom f) = {} ;
then f .: (product p) = f .: {} by RELAT_1:112
.= {} ;
then f .: (product p) c= the Element of Class (LimDomRel A) ;
hence ex a being Element of Class (LimDomRel A) st f .: (product p) c= a ; :: thesis: verum

end;

end;

end;

let p be FinSequence of Class (LimDomRel A); :: thesis: ( product p meets dom f implies product p c= dom f )
assume product p meets dom f ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not y in product p or y in dom f )
assume A31: y in product p ; :: thesis: 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 S₁[ set ] means $1 in dom f;
defpred S₂[ 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: S₁[x] by A30;
A38: for p1, q1 being FinSequence
for z1, z2 being set st S₁[(p1 ^ <*z1*>) ^ q1] & S₂[z1,z2] holds
S₁[(p1 ^ <*z2*>) ^ q1]

proof

let p1, q1 be FinSequence; :: thesis: for z1, z2 being set st S₁[(p1 ^ <*z1*>) ^ q1] & S₂[z1,z2] holds
S₁[(p1 ^ <*z2*>) ^ q1]
let z1, z2 be set ; :: thesis: ( S₁[(p1 ^ <*z1*>) ^ q1] & S₂[z1,z2] implies S₁[(p1 ^ <*z2*>) ^ q1] )
assume that
A39: (p1 ^ <*z1*>) ^ q1 in dom f and
A40: [z1,z2] in LimDomRel A ; :: thesis: S₁[(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 S₁[(p1 ^ <*z2*>) ^ q1] by A39, A40, A41, A42, Def4; :: thesis: verum

end;

A43: for i being Element of NAT st i in dom x holds
S₂[x . i,z . i]

proof

let i be Element of NAT ; :: thesis: ( i in dom x implies S₂[x . i,z . i] )
assume A44: i in dom x ; :: thesis: S₂[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 S₂[x . i,z . i] by A47, A48, EQREL_1:22; :: thesis: verum

end;

S₁[z] from PUA2MSS1:sch 4(A37, A36, A38, A43);
hence y in dom f ; :: thesis: verum