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;
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 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
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 ;
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 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;
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;
end;
end;
((p2 ") * p1) . j in Seg (len p2) by A34, FINSEQ_1:def 3;
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;
A39: len q1 = len p2 by A23, FINSEQ_1:6;
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 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) = 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 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;
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;
end;
end;
((p1 ") * p2) . j in Seg (len p1) by A46, FINSEQ_1:def 3;
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;
then P = Intersect (rng (MergeSequence (p2,q1))) by A15, A27, XBOOLE_0:def 10;
hence P in C2 by A10, A39; :: 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 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
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 ;
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 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;
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;
end;
end;
((p1 ") * p2) . j in Seg (len p1) by A72, FINSEQ_1:def 3;
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;
A77: len q1 = len p1 by A61, FINSEQ_1:6;
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 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) = 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 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;
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;
end;
end;
((p2 ") * p1) . j in Seg (len p2) by A84, FINSEQ_1:def 3;
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;
then P = Intersect (rng (MergeSequence (p1,q1))) by A53, A65, XBOOLE_0:def 10;
hence P in C1 by A7, A77; :: thesis: verum
end;
end;
hence C1 = C2 by SETFAM_1:31; :: thesis: verum