let C1, C2 be Subset-Family of X; ( 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 } )
; 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 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;
( ( P in C1 implies P in C2 ) & ( P in C2 implies P in C1 ) )thus
(
P in C1 implies
P in C2 )
( 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
;
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 ;
TARSKI:def 3 ( not z in rng (MergeSequence (p1,q)) or z in rng (MergeSequence (p2,q1)) )
assume
z in rng (MergeSequence (p1,q))
;
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 (MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = zper cases
( q . j = TRUE or q . j = FALSE )
by XBOOLEAN:def 3;
suppose A38:
q . j = FALSE
;
(MergeSequence (p2,q1)) . (((p2 ") * p1) . j) = zhence (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
;
verum 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;
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 ;
TARSKI:def 3 ( not z in rng (MergeSequence (p2,q1)) or z in rng (MergeSequence (p1,q)) )
assume
z in rng (MergeSequence (p2,q1))
;
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 (MergeSequence (p1,q)) . (((p1 ") * p2) . j) = zper cases
( q1 . j = TRUE or q1 . j = FALSE )
by XBOOLEAN:def 3;
suppose A50:
q1 . j = FALSE
;
(MergeSequence (p1,q)) . (((p1 ") * p2) . j) = zhence (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
;
verum 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;
verum
end;
then
P = Intersect (rng (MergeSequence (p2,q1)))
by A15, A27, XBOOLE_0:def 10;
hence
P in C2
by A10, A39;
verum
end; thus
(
P in C2 implies
P in C1 )
verumproof
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
;
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 ;
TARSKI:def 3 ( not z in rng (MergeSequence (p2,q)) or z in rng (MergeSequence (p1,q1)) )
assume
z in rng (MergeSequence (p2,q))
;
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 (MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = zper cases
( q . j = TRUE or q . j = FALSE )
by XBOOLEAN:def 3;
suppose A76:
q . j = FALSE
;
(MergeSequence (p1,q1)) . (((p1 ") * p2) . j) = zhence (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
;
verum 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;
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 ;
TARSKI:def 3 ( not z in rng (MergeSequence (p1,q1)) or z in rng (MergeSequence (p2,q)) )
assume
z in rng (MergeSequence (p1,q1))
;
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 (MergeSequence (p2,q)) . (((p2 ") * p1) . j) = zper cases
( q1 . j = TRUE or q1 . j = FALSE )
by XBOOLEAN:def 3;
suppose A88:
q1 . j = FALSE
;
(MergeSequence (p2,q)) . (((p2 ") * p1) . j) = zhence (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
;
verum 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;
verum
end;
then
P = Intersect (rng (MergeSequence (p1,q1)))
by A53, A65, XBOOLE_0:def 10;
hence
P in C1
by A7, A77;
verum
end; end;
hence
C1 = C2
by SETFAM_1:31; verum