let A be partial non-empty UAStr ; :: thesis: for P being a_partition of A holds P is_finer_than Class (LimDomRel A)
let P be a_partition of A; :: thesis: P is_finer_than Class (LimDomRel A)
consider EP being Equivalence_Relation of the carrier of A such that
A1: P = Class EP by EQREL_1:43;
let a be set ; :: according to SETFAM_1:def 2 :: thesis: ( not a in P or ex b₁ being set st
( b₁ in Class (LimDomRel A) & a c= b₁ ) )
assume a in P ; :: thesis: ex b₁ being set st
( b₁ in Class (LimDomRel A) & a c= b₁ )
then reconsider aa = a as Element of P ;
consider x being Element of aa;
take Class (LimDomRel A),x ; :: thesis: ( Class (LimDomRel A),x in Class (LimDomRel A) & a c= Class (LimDomRel A),x )
thus Class (LimDomRel A),x in Class (LimDomRel A) by EQREL_1:def 5; :: thesis: a c= Class (LimDomRel A),x
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in a or y in Class (LimDomRel A),x )
assume y in a ; :: thesis: y in Class (LimDomRel A),x
then reconsider y = y as Element of aa ;
reconsider x = x, y = y as Element of A ;
defpred S₁[ Element of NAT ] means EP c= (DomRel A) |^ A,$1;
A2: S₁[ 0 ]

proof

let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in EP or [x,y] in (DomRel A) |^ A,0 )
assume A3: [x,y] in EP ; :: thesis: [x,y] in (DomRel A) |^ A,0
then reconsider x = x, y = y as Element of A by ZFMISC_1:106;
reconsider a = Class EP,y as Element of P by A1, EQREL_1:def 5;
A4: x in a by A3, EQREL_1:27;
A5: y in a by EQREL_1:28;
for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )

proof

let f be operation of A; :: thesis: for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )
let p, q be FinSequence; :: thesis: ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )
A6: f is_exactly_partitable_wrt P by Def11;

now

let p, q be FinSequence; :: thesis: for x, y being Element of a st (p ^ <*x*>) ^ q in dom f holds
(p ^ <*y*>) ^ q in dom f
let x, y be Element of a; :: thesis: ( (p ^ <*x*>) ^ q in dom f implies (p ^ <*y*>) ^ q in dom f )
assume A7: (p ^ <*x*>) ^ q in dom f ; :: thesis: (p ^ <*y*>) ^ q in dom f
then (p ^ <*x*>) ^ q is FinSequence of the carrier of A by FINSEQ_1:def 11;
then consider pp being FinSequence of P such that
A8: (p ^ <*x*>) ^ q in product pp by Th7;
product pp meets dom f by A7, A8, XBOOLE_0:3;
then A9: product pp c= dom f by A6, Def10;
(p ^ <*y*>) ^ q in product pp by A8, Th27;
hence (p ^ <*y*>) ^ q in dom f by A9; :: thesis: verum

end;

hence ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) by A4, A5; :: thesis: verum

end;

then [x,y] in DomRel A by Def5;
hence [x,y] in (DomRel A) |^ A,0 by Th17; :: thesis: verum

end;

A10: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A11: EP c= (DomRel A) |^ A,i ; :: thesis: S₁[i + 1]
let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in EP or [x,y] in (DomRel A) |^ A,(i + 1) )
assume A12: [x,y] in EP ; :: thesis: [x,y] in (DomRel A) |^ A,(i + 1)
then reconsider x = x, y = y as Element of A by ZFMISC_1:106;
reconsider a = Class EP,y as Element of P by A1, EQREL_1:def 5;

now

let f be operation of A; :: thesis: for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ A,i
let p, q be FinSequence; :: thesis: ( (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f implies [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ A,i )
assume that
A13: (p ^ <*x*>) ^ q in dom f and
A14: (p ^ <*y*>) ^ q in dom f ; :: thesis: [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ A,i
(p ^ <*x*>) ^ q is FinSequence of the carrier of A by A13, FINSEQ_1:def 11;
then consider pp being FinSequence of P such that
A15: (p ^ <*x*>) ^ q in product pp by Th7;
f is_exactly_partitable_wrt P by Def11;
then f is_partitable_wrt P by Def10;
then consider c being Element of P such that
A16: f .: (product pp) c= c by Def9;
A17: x in a by A12, EQREL_1:27;
y in a by EQREL_1:28;
then A18: (p ^ <*y*>) ^ q in product pp by A15, A17, Th27;
A19: f . ((p ^ <*x*>) ^ q) in f .: (product pp) by A13, A15, FUNCT_1:def 12;
A20: f . ((p ^ <*y*>) ^ q) in f .: (product pp) by A14, A18, FUNCT_1:def 12;
ex x being set st
( x in the carrier of A & c = Class EP,x ) by A1, EQREL_1:def 5;
then [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in EP by A16, A19, A20, EQREL_1:30;
hence [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ A,i by A11; :: thesis: verum

end;

then [x,y] in ((DomRel A) |^ A,i) |^ A by A11, A12, Def6;
hence [x,y] in (DomRel A) |^ A,(i + 1) by Th18; :: thesis: verum

end;

A21: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A2, A10);

now

let i be Element of NAT ; :: thesis: [x,y] in (DomRel A) |^ A,i
ex x being set st
( x in the carrier of A & aa = Class EP,x ) by A1, EQREL_1:def 5;
then A22: [x,y] in EP by EQREL_1:30;
EP c= (DomRel A) |^ A,i by A21;
hence [x,y] in (DomRel A) |^ A,i by A22; :: thesis: verum

end;

then [x,y] in LimDomRel A by Def8;
then [y,x] in LimDomRel A by EQREL_1:12;
hence y in Class (LimDomRel A),x by EQREL_1:27; :: thesis: verum