let C1, C2 be Subset-Family of X; :: thesis: ( ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C1 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) & ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C2 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) implies C1 = C2 )

assume that

A3: ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C1 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) and

A4: ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C2 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) ; :: thesis: C1 = C2

consider p1 being FinSequence of bool X such that

A5: len p1 = card Y and

A6: rng p1 = Y and

A7: C1 = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 } by A3;

consider p2 being FinSequence of bool X such that

A8: len p2 = card Y and

A9: rng p2 = Y and

A10: C2 = { (Intersect (rng (MergeSequence (p2,q)))) where q is FinSequence of BOOLEAN : len q = len p2 } by A4;

A11: p2 is one-to-one by A8, A9, FINSEQ_4:62;

A12: p1 is one-to-one by A5, A6, FINSEQ_4:62;

( len p = card Y & rng p = Y & C1 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) & ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C2 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) implies C1 = C2 )

assume that

A3: ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C1 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) and

A4: ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C2 = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) ; :: thesis: C1 = C2

consider p1 being FinSequence of bool X such that

A5: len p1 = card Y and

A6: rng p1 = Y and

A7: C1 = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 } by A3;

consider p2 being FinSequence of bool X such that

A8: len p2 = card Y and

A9: rng p2 = Y and

A10: C2 = { (Intersect (rng (MergeSequence (p2,q)))) where q is FinSequence of BOOLEAN : len q = len p2 } by A4;

A11: p2 is one-to-one by A8, A9, FINSEQ_4:62;

A12: p1 is one-to-one by A5, A6, FINSEQ_4:62;

now :: thesis: for P being Subset of X holds

( ( P in C1 implies P in C2 ) & ( P in C2 implies P in C1 ) )

hence
C1 = C2
by SETFAM_1:31; :: thesis: verum( ( P in C1 implies P in C2 ) & ( P in C2 implies P in C1 ) )

let P be Subset of X; :: thesis: ( ( P in C1 implies P in C2 ) & ( P in C2 implies P in C1 ) )

thus ( P in C1 implies P in C2 ) :: thesis: ( P in C2 implies P in C1 )

end;thus ( P in C1 implies P in C2 ) :: thesis: ( P in C2 implies P in C1 )

proof

thus
( P in C2 implies P in C1 )
:: thesis: verum
p1 is Function of (dom p1),(rng p1)
by FUNCT_2:1;

then A13: p1 " is Function of (rng p1),(dom p1) by A12, FUNCT_2:25;

p2 is FinSequence of rng p1 by A6, A9, FINSEQ_1:def 4;

then A14: (p1 ") * p2 is FinSequence of dom p1 by A13, FINSEQ_2:32;

assume P in C1 ; :: thesis: P in C2

then consider q being FinSequence of BOOLEAN such that

A15: P = Intersect (rng (MergeSequence (p1,q))) and

A16: len q = len p1 by A7;

A17: dom p1 = Seg (len q) by A16, FINSEQ_1:def 3

.= dom q by FINSEQ_1:def 3 ;

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

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

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

A18: rng p2 = dom (p1 ") by A6, A9, A12, FUNCT_1:33;

then A19: dom ((p1 ") * p2) = dom p2 by RELAT_1:27;

rng ((p1 ") * p2) = rng (p1 ") by A18, RELAT_1:28

.= dom q by A12, A17, FUNCT_1:33 ;

then A20: dom (q * ((p1 ") * p2)) = dom p2 by A19, RELAT_1:27;

A21: rng p1 = dom (p2 ") by A6, A9, A11, FUNCT_1:33;

then A22: dom ((p2 ") * p1) = dom p1 by RELAT_1:27;

A23: Seg (len q1) = dom q1 by FINSEQ_1:def 3

.= dom p2 by A20, RELAT_1:36

.= Seg (len p2) by FINSEQ_1:def 3 ;

then A24: dom p2 = Seg (len q1) by FINSEQ_1:def 3

.= dom q1 by FINSEQ_1:def 3 ;

rng ((p2 ") * p1) = rng (p2 ") by A21, RELAT_1:28

.= dom q1 by A11, A24, FUNCT_1:33 ;

then A25: dom (q1 * ((p2 ") * p1)) = dom p1 by A22, RELAT_1:27;

A26: (q1 * (p2 ")) * p1 = ((q * (p1 ")) * p2) * ((p2 ") * p1) by RELAT_1:36

.= (q * (p1 ")) * (p2 * ((p2 ") * p1)) by RELAT_1:36

.= (q * (p1 ")) * ((p2 * (p2 ")) * p1) by RELAT_1:36

.= (q * (p1 ")) * ((id (rng p2)) * p1) by A11, FUNCT_1:39

.= (q * (p1 ")) * p1 by A6, A9, RELAT_1:54

.= q * ((p1 ") * p1) by RELAT_1:36

.= q * (id (dom p1)) by A12, FUNCT_1:39

.= q by A17, RELAT_1:52 ;

A27: rng (MergeSequence (p1,q)) c= rng (MergeSequence (p2,q1))

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

hence P in C2 by A10, A39; :: thesis: verum

end;then A13: p1 " is Function of (rng p1),(dom p1) by A12, FUNCT_2:25;

p2 is FinSequence of rng p1 by A6, A9, FINSEQ_1:def 4;

then A14: (p1 ") * p2 is FinSequence of dom p1 by A13, FINSEQ_2:32;

assume P in C1 ; :: thesis: P in C2

then consider q being FinSequence of BOOLEAN such that

A15: P = Intersect (rng (MergeSequence (p1,q))) and

A16: len q = len p1 by A7;

A17: dom p1 = Seg (len q) by A16, FINSEQ_1:def 3

.= dom q by FINSEQ_1:def 3 ;

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

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

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

A18: rng p2 = dom (p1 ") by A6, A9, A12, FUNCT_1:33;

then A19: dom ((p1 ") * p2) = dom p2 by RELAT_1:27;

rng ((p1 ") * p2) = rng (p1 ") by A18, RELAT_1:28

.= dom q by A12, A17, FUNCT_1:33 ;

then A20: dom (q * ((p1 ") * p2)) = dom p2 by A19, RELAT_1:27;

A21: rng p1 = dom (p2 ") by A6, A9, A11, FUNCT_1:33;

then A22: dom ((p2 ") * p1) = dom p1 by RELAT_1:27;

A23: Seg (len q1) = dom q1 by FINSEQ_1:def 3

.= dom p2 by A20, RELAT_1:36

.= Seg (len p2) by FINSEQ_1:def 3 ;

then A24: dom p2 = Seg (len q1) by FINSEQ_1:def 3

.= dom q1 by FINSEQ_1:def 3 ;

rng ((p2 ") * p1) = rng (p2 ") by A21, RELAT_1:28

.= dom q1 by A11, A24, FUNCT_1:33 ;

then A25: dom (q1 * ((p2 ") * p1)) = dom p1 by A22, RELAT_1:27;

A26: (q1 * (p2 ")) * p1 = ((q * (p1 ")) * p2) * ((p2 ") * p1) by RELAT_1:36

.= (q * (p1 ")) * (p2 * ((p2 ") * p1)) by RELAT_1:36

.= (q * (p1 ")) * ((p2 * (p2 ")) * p1) by RELAT_1:36

.= (q * (p1 ")) * ((id (rng p2)) * p1) by A11, FUNCT_1:39

.= (q * (p1 ")) * p1 by A6, A9, RELAT_1:54

.= q * ((p1 ") * p1) by RELAT_1:36

.= q * (id (dom p1)) by A12, FUNCT_1:39

.= q by A17, RELAT_1:52 ;

A27: rng (MergeSequence (p1,q)) c= rng (MergeSequence (p2,q1))

proof

A39:
len q1 = len p2
by A23, FINSEQ_1:6;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (MergeSequence (p1,q)) or z in rng (MergeSequence (p2,q1)) )

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

then consider j being Nat such that

A28: j in dom (MergeSequence (p1,q)) and

A29: (MergeSequence (p1,q)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p1,q))) by A28, FINSEQ_1:def 3;

then A30: j in Seg (len p1) by Def1;

then A31: j in dom (q1 * ((p2 ") * p1)) by A25, FINSEQ_1:def 3;

A32: j in dom p1 by A30, FINSEQ_1:def 3;

then A33: j in dom ((p2 ") * p1) by A21, RELAT_1:27;

then ((p2 ") * p1) . j in rng ((p2 ") * p1) by FUNCT_1:def 3;

then ((p2 ") * p1) . j in rng (p2 ") by FUNCT_1:14;

then A34: ((p2 ") * p1) . j in dom p2 by A11, FUNCT_1:33;

then reconsider pj = ((p2 ") * p1) . j as Element of NAT ;

A35: q . j = (q1 * ((p2 ") * p1)) . j by A26, RELAT_1:36

.= q1 . (((p2 ") * p1) . j) by A31, FUNCT_1:12 ;

then ((p2 ") * p1) . j in Seg (len (MergeSequence (p2,q1))) by Def1;

then ((p2 ") * p1) . j in dom (MergeSequence (p2,q1)) by FINSEQ_1:def 3;

hence z in rng (MergeSequence (p2,q1)) by A36, FUNCT_1:def 3; :: thesis: verum

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

then consider j being Nat such that

A28: j in dom (MergeSequence (p1,q)) and

A29: (MergeSequence (p1,q)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p1,q))) by A28, FINSEQ_1:def 3;

then A30: j in Seg (len p1) by Def1;

then A31: j in dom (q1 * ((p2 ") * p1)) by A25, FINSEQ_1:def 3;

A32: j in dom p1 by A30, FINSEQ_1:def 3;

then A33: j in dom ((p2 ") * p1) by A21, RELAT_1:27;

then ((p2 ") * p1) . j in rng ((p2 ") * p1) by FUNCT_1:def 3;

then ((p2 ") * p1) . j in rng (p2 ") by FUNCT_1:14;

then A34: ((p2 ") * p1) . j in dom p2 by A11, FUNCT_1:33;

then reconsider pj = ((p2 ") * p1) . j as Element of NAT ;

A35: q . j = (q1 * ((p2 ") * p1)) . j by A26, RELAT_1:36

.= q1 . (((p2 ") * p1) . j) by A31, FUNCT_1:12 ;

A36: now :: thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = zend;

((p2 ") * p1) . j in Seg (len p2)
by A34, FINSEQ_1:def 3;per cases
( q . j = TRUE or q . j = FALSE )
by XBOOLEAN:def 3;

end;

suppose A37:
q . j = TRUE
; :: thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = z

hence (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) =
p2 . pj
by A35, Th2

.= (p2 * ((p2 ") * p1)) . j by A33, FUNCT_1:13

.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36

.= ((id (rng p1)) * p1) . j by A6, A9, A11, FUNCT_1:39

.= p1 . j by RELAT_1:54

.= z by A29, A37, Th2 ;

:: thesis: verum

end;.= (p2 * ((p2 ") * p1)) . j by A33, FUNCT_1:13

.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36

.= ((id (rng p1)) * p1) . j by A6, A9, A11, FUNCT_1:39

.= p1 . j by RELAT_1:54

.= z by A29, A37, Th2 ;

:: thesis: verum

suppose A38:
q . j = FALSE
; :: thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = z

hence (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) =
X \ (p2 . pj)
by A34, A35, Th3

.= X \ ((p2 * ((p2 ") * p1)) . j) by A33, FUNCT_1:13

.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36

.= X \ (((id (rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1:39

.= X \ (p1 . j) by RELAT_1:54

.= z by A29, A32, Th3, A38 ;

:: thesis: verum

end;.= X \ ((p2 * ((p2 ") * p1)) . j) by A33, FUNCT_1:13

.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36

.= X \ (((id (rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1:39

.= X \ (p1 . j) by RELAT_1:54

.= z by A29, A32, Th3, A38 ;

:: thesis: verum

then ((p2 ") * p1) . j in Seg (len (MergeSequence (p2,q1))) by Def1;

then ((p2 ") * p1) . j in dom (MergeSequence (p2,q1)) by FINSEQ_1:def 3;

hence z in rng (MergeSequence (p2,q1)) by A36, FUNCT_1:def 3; :: thesis: verum

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

proof

then
P = Intersect (rng (MergeSequence (p2,q1)))
by A15, A27, XBOOLE_0:def 10;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (MergeSequence (p2,q1)) or z in rng (MergeSequence (p1,q)) )

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

then consider j being Nat such that

A40: j in dom (MergeSequence (p2,q1)) and

A41: (MergeSequence (p2,q1)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p2,q1))) by A40, FINSEQ_1:def 3;

then A42: j in Seg (len p2) by Def1;

then A43: j in dom (q * ((p1 ") * p2)) by A20, FINSEQ_1:def 3;

A44: j in dom p2 by A42, FINSEQ_1:def 3;

then A45: j in dom ((p1 ") * p2) by A18, RELAT_1:27;

then ((p1 ") * p2) . j in rng ((p1 ") * p2) by FUNCT_1:def 3;

then ((p1 ") * p2) . j in rng (p1 ") by FUNCT_1:14;

then A46: ((p1 ") * p2) . j in dom p1 by A12, FUNCT_1:33;

then reconsider pj = ((p1 ") * p2) . j as Element of NAT ;

A47: q1 . j = (q * ((p1 ") * p2)) . j by RELAT_1:36

.= q . (((p1 ") * p2) . j) by A43, FUNCT_1:12 ;

then ((p1 ") * p2) . j in Seg (len (MergeSequence (p1,q))) by Def1;

then ((p1 ") * p2) . j in dom (MergeSequence (p1,q)) by FINSEQ_1:def 3;

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

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

then consider j being Nat such that

A40: j in dom (MergeSequence (p2,q1)) and

A41: (MergeSequence (p2,q1)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p2,q1))) by A40, FINSEQ_1:def 3;

then A42: j in Seg (len p2) by Def1;

then A43: j in dom (q * ((p1 ") * p2)) by A20, FINSEQ_1:def 3;

A44: j in dom p2 by A42, FINSEQ_1:def 3;

then A45: j in dom ((p1 ") * p2) by A18, RELAT_1:27;

then ((p1 ") * p2) . j in rng ((p1 ") * p2) by FUNCT_1:def 3;

then ((p1 ") * p2) . j in rng (p1 ") by FUNCT_1:14;

then A46: ((p1 ") * p2) . j in dom p1 by A12, FUNCT_1:33;

then reconsider pj = ((p1 ") * p2) . j as Element of NAT ;

A47: q1 . j = (q * ((p1 ") * p2)) . j by RELAT_1:36

.= q . (((p1 ") * p2) . j) by A43, FUNCT_1:12 ;

A48: now :: thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = zend;

((p1 ") * p2) . j in Seg (len p1)
by A46, FINSEQ_1:def 3;per cases
( q1 . j = TRUE or q1 . j = FALSE )
by XBOOLEAN:def 3;

end;

suppose A49:
q1 . j = TRUE
; :: thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = z

hence (MergeSequence (p1,q)) . (((p1 ") * p2) . j) =
p1 . pj
by A47, Th2

.= (p1 * ((p1 ") * p2)) . j by A45, FUNCT_1:13

.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36

.= ((id (rng p2)) * p2) . j by A6, A9, A12, FUNCT_1:39

.= p2 . j by RELAT_1:54

.= z by A41, A49, Th2 ;

:: thesis: verum

end;.= (p1 * ((p1 ") * p2)) . j by A45, FUNCT_1:13

.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36

.= ((id (rng p2)) * p2) . j by A6, A9, A12, FUNCT_1:39

.= p2 . j by RELAT_1:54

.= z by A41, A49, Th2 ;

:: thesis: verum

suppose A50:
q1 . j = FALSE
; :: thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = z

hence (MergeSequence (p1,q)) . (((p1 ") * p2) . j) =
X \ (p1 . pj)
by A46, A47, Th3

.= X \ ((p1 * ((p1 ") * p2)) . j) by A45, FUNCT_1:13

.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36

.= X \ (((id (rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1:39

.= X \ (p2 . j) by RELAT_1:54

.= z by A41, A44, A50, Th3 ;

:: thesis: verum

end;.= X \ ((p1 * ((p1 ") * p2)) . j) by A45, FUNCT_1:13

.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36

.= X \ (((id (rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1:39

.= X \ (p2 . j) by RELAT_1:54

.= z by A41, A44, A50, Th3 ;

:: thesis: verum

then ((p1 ") * p2) . j in Seg (len (MergeSequence (p1,q))) by Def1;

then ((p1 ") * p2) . j in dom (MergeSequence (p1,q)) by FINSEQ_1:def 3;

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

hence P in C2 by A10, A39; :: thesis: verum

proof

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

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

p1 is FinSequence of rng p2 by A6, A9, FINSEQ_1:def 4;

then A52: (p2 ") * p1 is FinSequence of dom p2 by A51, FINSEQ_2:32;

assume P in C2 ; :: thesis: P in C1

then consider q being FinSequence of BOOLEAN such that

A53: P = Intersect (rng (MergeSequence (p2,q))) and

A54: len q = len p2 by A10;

A55: dom p2 = Seg (len q) by A54, FINSEQ_1:def 3

.= dom q by FINSEQ_1:def 3 ;

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

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

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

A56: rng p1 = dom (p2 ") by A6, A9, A11, FUNCT_1:33;

then A57: dom ((p2 ") * p1) = dom p1 by RELAT_1:27;

rng ((p2 ") * p1) = rng (p2 ") by A56, RELAT_1:28

.= dom q by A11, A55, FUNCT_1:33 ;

then A58: dom (q * ((p2 ") * p1)) = dom p1 by A57, RELAT_1:27;

A59: rng p2 = dom (p1 ") by A6, A9, A12, FUNCT_1:33;

then A60: dom ((p1 ") * p2) = dom p2 by RELAT_1:27;

A61: Seg (len q1) = dom q1 by FINSEQ_1:def 3

.= dom p1 by A58, RELAT_1:36

.= Seg (len p1) by FINSEQ_1:def 3 ;

then A62: dom p1 = Seg (len q1) by FINSEQ_1:def 3

.= dom q1 by FINSEQ_1:def 3 ;

rng ((p1 ") * p2) = rng (p1 ") by A59, RELAT_1:28

.= dom q1 by A12, A62, FUNCT_1:33 ;

then A63: dom (q1 * ((p1 ") * p2)) = dom p2 by A60, RELAT_1:27;

A64: (q1 * (p1 ")) * p2 = ((q * (p2 ")) * p1) * ((p1 ") * p2) by RELAT_1:36

.= (q * (p2 ")) * (p1 * ((p1 ") * p2)) by RELAT_1:36

.= (q * (p2 ")) * ((p1 * (p1 ")) * p2) by RELAT_1:36

.= (q * (p2 ")) * ((id (rng p1)) * p2) by A12, FUNCT_1:39

.= (q * (p2 ")) * p2 by A6, A9, RELAT_1:54

.= q * ((p2 ") * p2) by RELAT_1:36

.= q * (id (dom p2)) by A11, FUNCT_1:39

.= q by A55, RELAT_1:52 ;

A65: rng (MergeSequence (p2,q)) c= rng (MergeSequence (p1,q1))

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

hence P in C1 by A7, A77; :: thesis: verum

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

p1 is FinSequence of rng p2 by A6, A9, FINSEQ_1:def 4;

then A52: (p2 ") * p1 is FinSequence of dom p2 by A51, FINSEQ_2:32;

assume P in C2 ; :: thesis: P in C1

then consider q being FinSequence of BOOLEAN such that

A53: P = Intersect (rng (MergeSequence (p2,q))) and

A54: len q = len p2 by A10;

A55: dom p2 = Seg (len q) by A54, FINSEQ_1:def 3

.= dom q by FINSEQ_1:def 3 ;

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

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

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

A56: rng p1 = dom (p2 ") by A6, A9, A11, FUNCT_1:33;

then A57: dom ((p2 ") * p1) = dom p1 by RELAT_1:27;

rng ((p2 ") * p1) = rng (p2 ") by A56, RELAT_1:28

.= dom q by A11, A55, FUNCT_1:33 ;

then A58: dom (q * ((p2 ") * p1)) = dom p1 by A57, RELAT_1:27;

A59: rng p2 = dom (p1 ") by A6, A9, A12, FUNCT_1:33;

then A60: dom ((p1 ") * p2) = dom p2 by RELAT_1:27;

A61: Seg (len q1) = dom q1 by FINSEQ_1:def 3

.= dom p1 by A58, RELAT_1:36

.= Seg (len p1) by FINSEQ_1:def 3 ;

then A62: dom p1 = Seg (len q1) by FINSEQ_1:def 3

.= dom q1 by FINSEQ_1:def 3 ;

rng ((p1 ") * p2) = rng (p1 ") by A59, RELAT_1:28

.= dom q1 by A12, A62, FUNCT_1:33 ;

then A63: dom (q1 * ((p1 ") * p2)) = dom p2 by A60, RELAT_1:27;

A64: (q1 * (p1 ")) * p2 = ((q * (p2 ")) * p1) * ((p1 ") * p2) by RELAT_1:36

.= (q * (p2 ")) * (p1 * ((p1 ") * p2)) by RELAT_1:36

.= (q * (p2 ")) * ((p1 * (p1 ")) * p2) by RELAT_1:36

.= (q * (p2 ")) * ((id (rng p1)) * p2) by A12, FUNCT_1:39

.= (q * (p2 ")) * p2 by A6, A9, RELAT_1:54

.= q * ((p2 ") * p2) by RELAT_1:36

.= q * (id (dom p2)) by A11, FUNCT_1:39

.= q by A55, RELAT_1:52 ;

A65: rng (MergeSequence (p2,q)) c= rng (MergeSequence (p1,q1))

proof

A77:
len q1 = len p1
by A61, FINSEQ_1:6;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (MergeSequence (p2,q)) or z in rng (MergeSequence (p1,q1)) )

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

then consider j being Nat such that

A66: j in dom (MergeSequence (p2,q)) and

A67: (MergeSequence (p2,q)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p2,q))) by A66, FINSEQ_1:def 3;

then A68: j in Seg (len p2) by Def1;

then A69: j in dom (q1 * ((p1 ") * p2)) by A63, FINSEQ_1:def 3;

A70: j in dom p2 by A68, FINSEQ_1:def 3;

then A71: j in dom ((p1 ") * p2) by A59, RELAT_1:27;

then ((p1 ") * p2) . j in rng ((p1 ") * p2) by FUNCT_1:def 3;

then ((p1 ") * p2) . j in rng (p1 ") by FUNCT_1:14;

then A72: ((p1 ") * p2) . j in dom p1 by A12, FUNCT_1:33;

then reconsider pj = ((p1 ") * p2) . j as Element of NAT ;

A73: q . j = (q1 * ((p1 ") * p2)) . j by A64, RELAT_1:36

.= q1 . (((p1 ") * p2) . j) by A69, FUNCT_1:12 ;

then ((p1 ") * p2) . j in Seg (len (MergeSequence (p1,q1))) by Def1;

then ((p1 ") * p2) . j in dom (MergeSequence (p1,q1)) by FINSEQ_1:def 3;

hence z in rng (MergeSequence (p1,q1)) by A74, FUNCT_1:def 3; :: thesis: verum

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

then consider j being Nat such that

A66: j in dom (MergeSequence (p2,q)) and

A67: (MergeSequence (p2,q)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p2,q))) by A66, FINSEQ_1:def 3;

then A68: j in Seg (len p2) by Def1;

then A69: j in dom (q1 * ((p1 ") * p2)) by A63, FINSEQ_1:def 3;

A70: j in dom p2 by A68, FINSEQ_1:def 3;

then A71: j in dom ((p1 ") * p2) by A59, RELAT_1:27;

then ((p1 ") * p2) . j in rng ((p1 ") * p2) by FUNCT_1:def 3;

then ((p1 ") * p2) . j in rng (p1 ") by FUNCT_1:14;

then A72: ((p1 ") * p2) . j in dom p1 by A12, FUNCT_1:33;

then reconsider pj = ((p1 ") * p2) . j as Element of NAT ;

A73: q . j = (q1 * ((p1 ") * p2)) . j by A64, RELAT_1:36

.= q1 . (((p1 ") * p2) . j) by A69, FUNCT_1:12 ;

A74: now :: thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = zend;

((p1 ") * p2) . j in Seg (len p1)
by A72, FINSEQ_1:def 3;per cases
( q . j = TRUE or q . j = FALSE )
by XBOOLEAN:def 3;

end;

suppose A75:
q . j = TRUE
; :: thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = z

hence (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) =
p1 . pj
by A73, Th2

.= (p1 * ((p1 ") * p2)) . j by A71, FUNCT_1:13

.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36

.= ((id (rng p2)) * p2) . j by A6, A9, A12, FUNCT_1:39

.= p2 . j by RELAT_1:54

.= z by A67, A75, Th2 ;

:: thesis: verum

end;.= (p1 * ((p1 ") * p2)) . j by A71, FUNCT_1:13

.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36

.= ((id (rng p2)) * p2) . j by A6, A9, A12, FUNCT_1:39

.= p2 . j by RELAT_1:54

.= z by A67, A75, Th2 ;

:: thesis: verum

suppose A76:
q . j = FALSE
; :: thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = z

hence (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) =
X \ (p1 . pj)
by A72, A73, Th3

.= X \ ((p1 * ((p1 ") * p2)) . j) by A71, FUNCT_1:13

.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36

.= X \ (((id (rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1:39

.= X \ (p2 . j) by RELAT_1:54

.= z by A67, A70, A76, Th3 ;

:: thesis: verum

end;.= X \ ((p1 * ((p1 ") * p2)) . j) by A71, FUNCT_1:13

.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36

.= X \ (((id (rng p2)) * p2) . j) by A6, A9, A12, FUNCT_1:39

.= X \ (p2 . j) by RELAT_1:54

.= z by A67, A70, A76, Th3 ;

:: thesis: verum

then ((p1 ") * p2) . j in Seg (len (MergeSequence (p1,q1))) by Def1;

then ((p1 ") * p2) . j in dom (MergeSequence (p1,q1)) by FINSEQ_1:def 3;

hence z in rng (MergeSequence (p1,q1)) by A74, FUNCT_1:def 3; :: thesis: verum

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

proof

then
P = Intersect (rng (MergeSequence (p1,q1)))
by A53, A65, XBOOLE_0:def 10;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (MergeSequence (p1,q1)) or z in rng (MergeSequence (p2,q)) )

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

then consider j being Nat such that

A78: j in dom (MergeSequence (p1,q1)) and

A79: (MergeSequence (p1,q1)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p1,q1))) by A78, FINSEQ_1:def 3;

then A80: j in Seg (len p1) by Def1;

then A81: j in dom (q * ((p2 ") * p1)) by A58, FINSEQ_1:def 3;

A82: j in dom p1 by A80, FINSEQ_1:def 3;

then A83: j in dom ((p2 ") * p1) by A56, RELAT_1:27;

then ((p2 ") * p1) . j in rng ((p2 ") * p1) by FUNCT_1:def 3;

then ((p2 ") * p1) . j in rng (p2 ") by FUNCT_1:14;

then A84: ((p2 ") * p1) . j in dom p2 by A11, FUNCT_1:33;

then reconsider pj = ((p2 ") * p1) . j as Element of NAT ;

A85: q1 . j = (q * ((p2 ") * p1)) . j by RELAT_1:36

.= q . (((p2 ") * p1) . j) by A81, FUNCT_1:12 ;

then ((p2 ") * p1) . j in Seg (len (MergeSequence (p2,q))) by Def1;

then ((p2 ") * p1) . j in dom (MergeSequence (p2,q)) by FINSEQ_1:def 3;

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

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

then consider j being Nat such that

A78: j in dom (MergeSequence (p1,q1)) and

A79: (MergeSequence (p1,q1)) . j = z by FINSEQ_2:10;

j in Seg (len (MergeSequence (p1,q1))) by A78, FINSEQ_1:def 3;

then A80: j in Seg (len p1) by Def1;

then A81: j in dom (q * ((p2 ") * p1)) by A58, FINSEQ_1:def 3;

A82: j in dom p1 by A80, FINSEQ_1:def 3;

then A83: j in dom ((p2 ") * p1) by A56, RELAT_1:27;

then ((p2 ") * p1) . j in rng ((p2 ") * p1) by FUNCT_1:def 3;

then ((p2 ") * p1) . j in rng (p2 ") by FUNCT_1:14;

then A84: ((p2 ") * p1) . j in dom p2 by A11, FUNCT_1:33;

then reconsider pj = ((p2 ") * p1) . j as Element of NAT ;

A85: q1 . j = (q * ((p2 ") * p1)) . j by RELAT_1:36

.= q . (((p2 ") * p1) . j) by A81, FUNCT_1:12 ;

A86: now :: thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = zend;

((p2 ") * p1) . j in Seg (len p2)
by A84, FINSEQ_1:def 3;per cases
( q1 . j = TRUE or q1 . j = FALSE )
by XBOOLEAN:def 3;

end;

suppose A87:
q1 . j = TRUE
; :: thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = z

hence (MergeSequence (p2,q)) . (((p2 ") * p1) . j) =
p2 . pj
by A85, Th2

.= (p2 * ((p2 ") * p1)) . j by A83, FUNCT_1:13

.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36

.= ((id (rng p1)) * p1) . j by A6, A9, A11, FUNCT_1:39

.= p1 . j by RELAT_1:54

.= z by A79, A87, Th2 ;

:: thesis: verum

end;.= (p2 * ((p2 ") * p1)) . j by A83, FUNCT_1:13

.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36

.= ((id (rng p1)) * p1) . j by A6, A9, A11, FUNCT_1:39

.= p1 . j by RELAT_1:54

.= z by A79, A87, Th2 ;

:: thesis: verum

suppose A88:
q1 . j = FALSE
; :: thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = z

hence (MergeSequence (p2,q)) . (((p2 ") * p1) . j) =
X \ (p2 . pj)
by A84, A85, Th3

.= X \ ((p2 * ((p2 ") * p1)) . j) by A83, FUNCT_1:13

.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36

.= X \ (((id (rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1:39

.= X \ (p1 . j) by RELAT_1:54

.= z by A79, A82, A88, Th3 ;

:: thesis: verum

end;.= X \ ((p2 * ((p2 ") * p1)) . j) by A83, FUNCT_1:13

.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36

.= X \ (((id (rng p1)) * p1) . j) by A6, A9, A11, FUNCT_1:39

.= X \ (p1 . j) by RELAT_1:54

.= z by A79, A82, A88, Th3 ;

:: thesis: verum

then ((p2 ") * p1) . j in Seg (len (MergeSequence (p2,q))) by Def1;

then ((p2 ") * p1) . j in dom (MergeSequence (p2,q)) by FINSEQ_1:def 3;

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

hence P in C1 by A7, A77; :: thesis: verum