let X be set ; :: thesis: for Y, Z being finite Subset-Family of X st Z c= Y holds

Components Y is_finer_than Components Z

let Y, Z be finite Subset-Family of X; :: thesis: ( Z c= Y implies Components Y is_finer_than Components Z )

assume A1: Z c= Y ; :: thesis: Components Y is_finer_than Components Z

Components Y is_finer_than Components Z

let Y, Z be finite Subset-Family of X; :: thesis: ( Z c= Y implies Components Y is_finer_than Components Z )

assume A1: Z c= Y ; :: thesis: Components Y is_finer_than Components Z

now :: thesis: for V being set st V in Components Y holds

ex W being set st

( W in Components Z & V c= W )

hence
Components Y is_finer_than Components Z
by SETFAM_1:def 2; :: thesis: verumex W being set st

( W in Components Z & V c= W )

let V be set ; :: thesis: ( V in Components Y implies ex W being set st

( W in Components Z & V c= W ) )

consider p being FinSequence of bool X such that

A2: len p = card Y and

A3: rng p = Y and

A4: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;

consider p1 being FinSequence of bool X such that

len p1 = card Z and

A5: rng p1 = Z and

A6: Components Z = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 } by Def2;

A7: p1 is FinSequence of rng p by A1, A3, A5, FINSEQ_1:def 4;

assume V in Components Y ; :: thesis: ex W being set st

( W in Components Z & V c= W )

then consider q being FinSequence of BOOLEAN such that

A8: V = Intersect (rng (MergeSequence (p,q))) and

A9: len q = len p by A4;

dom p = dom q by A9, FINSEQ_3:29;

then A10: q is Function of (dom p),BOOLEAN by FINSEQ_2:26;

A11: p is one-to-one by A2, A3, FINSEQ_4:62;

then A12: rng p1 c= dom (p ") by A1, A3, A5, FUNCT_1:33;

rng (p ") = dom p by A11, FUNCT_1:33

.= dom q by A9, FINSEQ_3:29 ;

then A13: rng ((p ") * p1) c= dom q by RELAT_1:26;

p is Function of (dom p),(rng p) by FUNCT_2:1;

then p " is Function of (rng p),(dom p) by A11, FUNCT_2:25;

then (p ") * p1 is FinSequence of dom p by A7, FINSEQ_2:32;

then q * ((p ") * p1) is FinSequence of BOOLEAN by A10, FINSEQ_2:32;

then reconsider q1 = (q * (p ")) * p1 as FinSequence of BOOLEAN by RELAT_1:36;

reconsider W = Intersect (rng (MergeSequence (p1,q1))) as set ;

take W = W; :: thesis: ( W in Components Z & V c= W )

dom q1 = dom (q * ((p ") * p1)) by RELAT_1:36

.= dom ((p ") * p1) by A13, RELAT_1:27

.= dom p1 by A12, RELAT_1:27 ;

then len q1 = len p1 by FINSEQ_3:29;

hence W in Components Z by A6; :: thesis: V c= W

rng (MergeSequence (p1,q1)) c= rng (MergeSequence (p,q))

end;( W in Components Z & V c= W ) )

consider p being FinSequence of bool X such that

A2: len p = card Y and

A3: rng p = Y and

A4: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;

consider p1 being FinSequence of bool X such that

len p1 = card Z and

A5: rng p1 = Z and

A6: Components Z = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 } by Def2;

A7: p1 is FinSequence of rng p by A1, A3, A5, FINSEQ_1:def 4;

assume V in Components Y ; :: thesis: ex W being set st

( W in Components Z & V c= W )

then consider q being FinSequence of BOOLEAN such that

A8: V = Intersect (rng (MergeSequence (p,q))) and

A9: len q = len p by A4;

dom p = dom q by A9, FINSEQ_3:29;

then A10: q is Function of (dom p),BOOLEAN by FINSEQ_2:26;

A11: p is one-to-one by A2, A3, FINSEQ_4:62;

then A12: rng p1 c= dom (p ") by A1, A3, A5, FUNCT_1:33;

rng (p ") = dom p by A11, FUNCT_1:33

.= dom q by A9, FINSEQ_3:29 ;

then A13: rng ((p ") * p1) c= dom q by RELAT_1:26;

p is Function of (dom p),(rng p) by FUNCT_2:1;

then p " is Function of (rng p),(dom p) by A11, FUNCT_2:25;

then (p ") * p1 is FinSequence of dom p by A7, FINSEQ_2:32;

then q * ((p ") * p1) is FinSequence of BOOLEAN by A10, FINSEQ_2:32;

then reconsider q1 = (q * (p ")) * p1 as FinSequence of BOOLEAN by RELAT_1:36;

reconsider W = Intersect (rng (MergeSequence (p1,q1))) as set ;

take W = W; :: thesis: ( W in Components Z & V c= W )

dom q1 = dom (q * ((p ") * p1)) by RELAT_1:36

.= dom ((p ") * p1) by A13, RELAT_1:27

.= dom p1 by A12, RELAT_1:27 ;

then len q1 = len p1 by FINSEQ_3:29;

hence W in Components Z by A6; :: thesis: V c= W

rng (MergeSequence (p1,q1)) c= rng (MergeSequence (p,q))

proof

hence
V c= W
by A8, SETFAM_1:44; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (MergeSequence (p1,q1)) or z in rng (MergeSequence (p,q)) )

assume z in rng (MergeSequence (p1,q1)) ; :: thesis: z in rng (MergeSequence (p,q))

then consider i being Nat such that

A14: i in dom (MergeSequence (p1,q1)) and

A15: (MergeSequence (p1,q1)) . i = z by FINSEQ_2:10;

A16: i in dom p1 by A14, Th1;

then A17: i in dom ((p ") * p1) by A12, RELAT_1:27;

then ((p ") * p1) . i in rng ((p ") * p1) by FUNCT_1:def 3;

then A18: ((p ") * p1) . i in rng (p ") by FUNCT_1:14;

then A19: ((p ") * p1) . i in dom p by A11, FUNCT_1:33;

then reconsider j = ((p ") * p1) . i as Element of NAT ;

A20: q . j = (q * ((p ") * p1)) . i by A17, FUNCT_1:13

.= q1 . i by RELAT_1:36 ;

A21: p1 is Function of (dom p1),(rng p) by A1, A3, A5, FUNCT_2:2;

A22: j in dom p by A11, A18, FUNCT_1:33;

hence z in rng (MergeSequence (p,q)) by A23, FUNCT_1:def 3; :: thesis: verum

end;assume z in rng (MergeSequence (p1,q1)) ; :: thesis: z in rng (MergeSequence (p,q))

then consider i being Nat such that

A14: i in dom (MergeSequence (p1,q1)) and

A15: (MergeSequence (p1,q1)) . i = z by FINSEQ_2:10;

A16: i in dom p1 by A14, Th1;

then A17: i in dom ((p ") * p1) by A12, RELAT_1:27;

then ((p ") * p1) . i in rng ((p ") * p1) by FUNCT_1:def 3;

then A18: ((p ") * p1) . i in rng (p ") by FUNCT_1:14;

then A19: ((p ") * p1) . i in dom p by A11, FUNCT_1:33;

then reconsider j = ((p ") * p1) . i as Element of NAT ;

A20: q . j = (q * ((p ") * p1)) . i by A17, FUNCT_1:13

.= q1 . i by RELAT_1:36 ;

A21: p1 is Function of (dom p1),(rng p) by A1, A3, A5, FUNCT_2:2;

A22: j in dom p by A11, A18, FUNCT_1:33;

A23: now :: thesis: (MergeSequence (p,q)) . j = zend;

j in dom (MergeSequence (p,q))
by A19, Th1;per cases
( q . j = TRUE or q . j = FALSE )
by XBOOLEAN:def 3;

end;

suppose A24:
q . j = TRUE
; :: thesis: (MergeSequence (p,q)) . j = z

hence (MergeSequence (p,q)) . j =
p . j
by Th2

.= (p * ((p ") * p1)) . i by A17, FUNCT_1:13

.= ((p * (p ")) * p1) . i by RELAT_1:36

.= ((id (rng p)) * p1) . i by A11, FUNCT_1:39

.= p1 . i by A21, FUNCT_2:17

.= z by A15, A20, A24, Th2 ;

:: thesis: verum

end;.= (p * ((p ") * p1)) . i by A17, FUNCT_1:13

.= ((p * (p ")) * p1) . i by RELAT_1:36

.= ((id (rng p)) * p1) . i by A11, FUNCT_1:39

.= p1 . i by A21, FUNCT_2:17

.= z by A15, A20, A24, Th2 ;

:: thesis: verum

suppose A25:
q . j = FALSE
; :: thesis: (MergeSequence (p,q)) . j = z

hence (MergeSequence (p,q)) . j =
X \ (p . j)
by A22, Th3

.= X \ ((p * ((p ") * p1)) . i) by A17, FUNCT_1:13

.= X \ (((p * (p ")) * p1) . i) by RELAT_1:36

.= X \ (((id (rng p)) * p1) . i) by A11, FUNCT_1:39

.= X \ (p1 . i) by A21, FUNCT_2:17

.= z by A15, A16, A20, A25, Th3 ;

:: thesis: verum

end;.= X \ ((p * ((p ") * p1)) . i) by A17, FUNCT_1:13

.= X \ (((p * (p ")) * p1) . i) by RELAT_1:36

.= X \ (((id (rng p)) * p1) . i) by A11, FUNCT_1:39

.= X \ (p1 . i) by A21, FUNCT_2:17

.= z by A15, A16, A20, A25, Th3 ;

:: thesis: verum

hence z in rng (MergeSequence (p,q)) by A23, FUNCT_1:def 3; :: thesis: verum