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 9,PUA2MSS1:def 10 :: 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₂
consider a0 being 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 set such that
A1: ( x in product p & x in dom f ) by XBOOLE_0:3;
f . x in the carrier of A by A1, PARTFUN1:27;
then reconsider a = Class (LimDomRel A),(f . x) as Element of Class (LimDomRel A) by EQREL_1:def 5;
take a = a; :: thesis: f .: (product p) c= a
thus f .: (product p) c= a :: thesis: verum

proof

let y be set ; :: 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 set such that
A2: ( z in dom f & z in product p & y = f . z ) by FUNCT_1:def 12;
product p c= Funcs (dom p),(Union p) by FUNCT_6:10;
then A3: ( ex f being Function st
( x = f & dom f = dom p & rng f c= Union p ) & ex f being Function st
( z = f & dom f = dom p & rng f c= Union p ) ) by A1, A2, FUNCT_2:def 2;
then reconsider x = x, z = z as Function ;
A4: dom p = Seg (len p) by FINSEQ_1:def 3;
then reconsider x = x, z = z as FinSequence by A3, 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 & len z = len p ) by A3, A4, FINSEQ_1:def 3;
then A5: len x = len z ;
A6: S₁[x] by A1, EQREL_1:28, PARTFUN1:27;
A7: 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 A8: ( (p1 ^ <*z1*>) ^ q1 in dom f & f . ((p1 ^ <*z1*>) ^ q1) in a & [z1,z2] in LimDomRel A ) ; :: thesis: S₁[(p1 ^ <*z2*>) ^ q1]
then A9: [(f . ((p1 ^ <*z1*>) ^ q1)),(f . x)] in LimDomRel A by EQREL_1:27;
LimDomRel A c= DomRel A by Th23;
then A10: ( z1 in the carrier of A & z2 in the carrier of A & [z1,z2] in DomRel A ) by A8, ZFMISC_1:106;
hence A11: (p1 ^ <*z2*>) ^ q1 in dom f by A8, Def5; :: thesis: f . ((p1 ^ <*z2*>) ^ q1) in a
then A12: ( f . ((p1 ^ <*z1*>) ^ q1) in rng f & f . ((p1 ^ <*z2*>) ^ q1) in rng f & rng f c= the carrier of A ) by A8, FUNCT_1:def 5;

now

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 A8, A10, Def8;
then [z1,z2] in ((DomRel A) |^ A,i) |^ A by Th18;
then ( [(f . ((p1 ^ <*z1*>) ^ q1)),(f . ((p1 ^ <*z2*>) ^ q1))] in (DomRel A) |^ A,i & (DomRel A) |^ A,i is total & (DomRel A) |^ A,i is symmetric & (DomRel A) |^ A,i is transitive ) by A8, A10, A11, Def6, Th22;
hence [(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in (DomRel A) |^ A,i by EQREL_1:12; :: thesis: verum

end;

then [(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in LimDomRel A by A12, Def8;
then [(f . ((p1 ^ <*z2*>) ^ q1)),(f . x)] in LimDomRel A by A9, EQREL_1:13;
hence f . ((p1 ^ <*z2*>) ^ q1) in a by EQREL_1:27; :: thesis: verum

end;

A13: 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 A14: i in dom x ; :: thesis: S₂[x . i,z . i]
then ( p . i in rng p & rng p c= Class (LimDomRel A) ) by A3, FUNCT_1:def 5;
then reconsider a = p . i as Element of Class (LimDomRel A) ;
( ex g being Function st
( x = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) & ex g being Function st
( z = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) ) by A1, A2, CARD_3:def 5;
then ( ex b being set st
( b in the carrier of A & a = Class (LimDomRel A),b ) & x . i in a & z . i in a ) by A14, EQREL_1:def 5;
hence S₂[x . i,z . i] by EQREL_1:30; :: thesis: verum

end;

S₁[z] from PUA2MSS1:sch 4(A6, A5, A7, A13);
hence y in a by A2; :: 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) = {} by XBOOLE_0:def 7;
then f .: (product p) = f .: {} by RELAT_1:145
.= {} by RELAT_1:149 ;
then f .: (product p) c= a0 by XBOOLE_1:2;
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 set such that
A15: ( x in product p & x in dom f ) by XBOOLE_0:3;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in product p or y in dom f )
assume A16: y in product p ; :: thesis: y in dom f
product p c= Funcs (dom p),(Union p) by FUNCT_6:10;
then A17: ( ex f being Function st
( x = f & dom f = dom p & rng f c= Union p ) & ex f being Function st
( y = f & dom f = dom p & rng f c= Union p ) ) by A15, A16, FUNCT_2:def 2;
then reconsider x = x, z = y as Function ;
A18: dom p = Seg (len p) by FINSEQ_1:def 3;
then reconsider x = x, z = z as FinSequence by A17, 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 & len z = len p ) by A17, A18, FINSEQ_1:def 3;
then A19: len x = len z ;
A20: S₁[x] by A15;
A21: 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 A22: ( (p1 ^ <*z1*>) ^ q1 in dom f & [z1,z2] in LimDomRel A ) ; :: thesis: S₁[(p1 ^ <*z2*>) ^ q1]
LimDomRel A c= DomRel A by Th23;
then ( z1 in the carrier of A & z2 in the carrier of A & [z1,z2] in DomRel A ) by A22, ZFMISC_1:106;
hence S₁[(p1 ^ <*z2*>) ^ q1] by A22, Def5; :: 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 & rng p c= Class (LimDomRel A) ) by A17, FUNCT_1:def 5;
then reconsider a = p . i as Element of Class (LimDomRel A) ;
( ex g being Function st
( x = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) & ex g being Function st
( z = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) ) by A15, A16, CARD_3:def 5;
then ( ex b being set st
( b in the carrier of A & a = Class (LimDomRel A),b ) & x . i in a & z . i in a ) by A24, EQREL_1:def 5;
hence S₂[x . i,z . i] by EQREL_1:30; :: thesis: verum

end;

S₁[z] from PUA2MSS1:sch 4(A20, A19, A21, A23);
hence y in dom f ; :: thesis: verum