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 ;
A12: p1 is one-to-one by ;
now :: thesis: for P being Subset of X holds
( ( 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 )
proof
p1 is Function of (dom p1),(rng p1) by FUNCT_2:1;
then A13: p1 " is Function of (rng p1),(dom p1) by ;
p2 is FinSequence of rng p1 by ;
then A14: (p1 ") * p2 is FinSequence of dom p1 by ;
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
.= 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 ;
then reconsider q1 = (q * (p1 ")) * p2 as FinSequence of BOOLEAN by RELAT_1:36;
A18: rng p2 = dom (p1 ") by ;
then A19: dom ((p1 ") * p2) = dom p2 by RELAT_1:27;
rng ((p1 ") * p2) = rng (p1 ") by
.= dom q by ;
then A20: dom (q * ((p1 ") * p2)) = dom p2 by ;
A21: rng p1 = dom (p2 ") by ;
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
.= 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
.= dom q1 by ;
then A25: dom (q1 * ((p2 ") * p1)) = dom p1 by ;
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
.= (q * (p1 ")) * p1 by
.= q * ((p1 ") * p1) by RELAT_1:36
.= q * (id (dom p1)) by
.= q by ;
A27: rng (MergeSequence (p1,q)) c= rng (MergeSequence (p2,q1))
proof
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 ;
then A30: j in Seg (len p1) by Def1;
then A31: j in dom (q1 * ((p2 ") * p1)) by ;
A32: j in dom p1 by ;
then A33: j in dom ((p2 ") * p1) by ;
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 ;
then reconsider pj = ((p2 ") * p1) . j as Element of NAT ;
A35: q . j = (q1 * ((p2 ") * p1)) . j by
.= q1 . (((p2 ") * p1) . j) by ;
A36: now :: thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = z
per cases ( q . j = TRUE or q . j = FALSE ) by XBOOLEAN:def 3;
suppose A37: q . j = TRUE ; :: thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = p2 . pj by
.= (p2 * ((p2 ") * p1)) . j by
.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36
.= ((id (rng p1)) * p1) . j by
.= p1 . j by RELAT_1:54
.= z by ;
:: thesis: verum
end;
suppose A38: q . j = FALSE ; :: thesis: (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = X \ (p2 . pj) by
.= X \ ((p2 * ((p2 ") * p1)) . j) by
.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36
.= X \ (((id (rng p1)) * p1) . j) by
.= X \ (p1 . j) by RELAT_1:54
.= z by A29, A32, Th3, A38 ;
:: thesis: verum
end;
end;
end;
((p2 ") * p1) . j in Seg (len p2) by ;
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 ; :: thesis: verum
end;
A39: len q1 = len p2 by ;
rng (MergeSequence (p2,q1)) c= rng (MergeSequence (p1,q))
proof
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 ;
then A42: j in Seg (len p2) by Def1;
then A43: j in dom (q * ((p1 ") * p2)) by ;
A44: j in dom p2 by ;
then A45: j in dom ((p1 ") * p2) by ;
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 ;
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 ;
A48: now :: thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = z
per cases ( q1 . j = TRUE or q1 . j = FALSE ) by XBOOLEAN:def 3;
suppose A49: q1 . j = TRUE ; :: thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = p1 . pj by
.= (p1 * ((p1 ") * p2)) . j by
.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36
.= ((id (rng p2)) * p2) . j by
.= p2 . j by RELAT_1:54
.= z by ;
:: thesis: verum
end;
suppose A50: q1 . j = FALSE ; :: thesis: (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = X \ (p1 . pj) by
.= X \ ((p1 * ((p1 ") * p2)) . j) by
.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36
.= X \ (((id (rng p2)) * p2) . j) by
.= X \ (p2 . j) by RELAT_1:54
.= z by A41, A44, A50, Th3 ;
:: thesis: verum
end;
end;
end;
((p1 ") * p2) . j in Seg (len p1) by ;
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 ; :: thesis: verum
end;
then P = Intersect (rng (MergeSequence (p2,q1))) by ;
hence P in C2 by ; :: thesis: verum
end;
thus ( P in C2 implies P in C1 ) :: 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 ;
p1 is FinSequence of rng p2 by ;
then A52: (p2 ") * p1 is FinSequence of dom p2 by ;
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
.= 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 ;
then reconsider q1 = (q * (p2 ")) * p1 as FinSequence of BOOLEAN by RELAT_1:36;
A56: rng p1 = dom (p2 ") by ;
then A57: dom ((p2 ") * p1) = dom p1 by RELAT_1:27;
rng ((p2 ") * p1) = rng (p2 ") by
.= dom q by ;
then A58: dom (q * ((p2 ") * p1)) = dom p1 by ;
A59: rng p2 = dom (p1 ") by ;
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
.= 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
.= dom q1 by ;
then A63: dom (q1 * ((p1 ") * p2)) = dom p2 by ;
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
.= (q * (p2 ")) * p2 by
.= q * ((p2 ") * p2) by RELAT_1:36
.= q * (id (dom p2)) by
.= q by ;
A65: rng (MergeSequence (p2,q)) c= rng (MergeSequence (p1,q1))
proof
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 ;
then A68: j in Seg (len p2) by Def1;
then A69: j in dom (q1 * ((p1 ") * p2)) by ;
A70: j in dom p2 by ;
then A71: j in dom ((p1 ") * p2) by ;
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 ;
then reconsider pj = ((p1 ") * p2) . j as Element of NAT ;
A73: q . j = (q1 * ((p1 ") * p2)) . j by
.= q1 . (((p1 ") * p2) . j) by ;
A74: now :: thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = z
per cases ( q . j = TRUE or q . j = FALSE ) by XBOOLEAN:def 3;
suppose A75: q . j = TRUE ; :: thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = p1 . pj by
.= (p1 * ((p1 ") * p2)) . j by
.= ((p1 * (p1 ")) * p2) . j by RELAT_1:36
.= ((id (rng p2)) * p2) . j by
.= p2 . j by RELAT_1:54
.= z by ;
:: thesis: verum
end;
suppose A76: q . j = FALSE ; :: thesis: (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = z
hence (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = X \ (p1 . pj) by
.= X \ ((p1 * ((p1 ") * p2)) . j) by
.= X \ (((p1 * (p1 ")) * p2) . j) by RELAT_1:36
.= X \ (((id (rng p2)) * p2) . j) by
.= X \ (p2 . j) by RELAT_1:54
.= z by A67, A70, A76, Th3 ;
:: thesis: verum
end;
end;
end;
((p1 ") * p2) . j in Seg (len p1) by ;
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 ; :: thesis: verum
end;
A77: len q1 = len p1 by ;
rng (MergeSequence (p1,q1)) c= rng (MergeSequence (p2,q))
proof
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 ;
then A80: j in Seg (len p1) by Def1;
then A81: j in dom (q * ((p2 ") * p1)) by ;
A82: j in dom p1 by ;
then A83: j in dom ((p2 ") * p1) by ;
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 ;
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 ;
A86: now :: thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = z
per cases ( q1 . j = TRUE or q1 . j = FALSE ) by XBOOLEAN:def 3;
suppose A87: q1 . j = TRUE ; :: thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = p2 . pj by
.= (p2 * ((p2 ") * p1)) . j by
.= ((p2 * (p2 ")) * p1) . j by RELAT_1:36
.= ((id (rng p1)) * p1) . j by
.= p1 . j by RELAT_1:54
.= z by ;
:: thesis: verum
end;
suppose A88: q1 . j = FALSE ; :: thesis: (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = z
hence (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = X \ (p2 . pj) by
.= X \ ((p2 * ((p2 ") * p1)) . j) by
.= X \ (((p2 * (p2 ")) * p1) . j) by RELAT_1:36
.= X \ (((id (rng p1)) * p1) . j) by
.= X \ (p1 . j) by RELAT_1:54
.= z by A79, A82, A88, Th3 ;
:: thesis: verum
end;
end;
end;
((p2 ") * p1) . j in Seg (len p2) by ;
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 ; :: thesis: verum
end;
then P = Intersect (rng (MergeSequence (p1,q1))) by ;
hence P in C1 by ; :: thesis: verum
end;
end;
hence C1 = C2 by SETFAM_1:31; :: thesis: verum