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;
now A11:
p1 is
one-to-one
by A5, A6, FINSEQ_4:77;
A12:
p2 is
one-to-one
by A8, A9, FINSEQ_4:77;
now 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
assume
P in C1
;
:: thesis: P in C2
then consider q being
FinSequence of
BOOLEAN such that A13:
P = Intersect (rng (MergeSequence p1,q))
and A14:
len q = len p1
by A7;
A15:
dom p1 =
Seg (len q)
by A14, FINSEQ_1:def 3
.=
dom q
by FINSEQ_1:def 3
;
A16:
p2 is
FinSequence of
rng p1
by A6, A9, FINSEQ_1:def 4;
A17:
q is
Function of
(dom p1),
BOOLEAN
by A15, FINSEQ_2:30;
p1 is
Function of
(dom p1),
(rng p1)
by FUNCT_2:3;
then
p1 " is
Function of
(rng p1),
(dom p1)
by A11, FUNCT_2:31;
then
(p1 " ) * p2 is
FinSequence of
dom p1
by A16, FINSEQ_2:36;
then
q * ((p1 " ) * p2) is
FinSequence of
BOOLEAN
by A17, FINSEQ_2:36;
then reconsider q1 =
(q * (p1 " )) * p2 as
FinSequence of
BOOLEAN by RELAT_1:55;
A18:
(q1 * (p2 " )) * p1 =
((q * (p1 " )) * p2) * ((p2 " ) * p1)
by RELAT_1:55
.=
(q * (p1 " )) * (p2 * ((p2 " ) * p1))
by RELAT_1:55
.=
(q * (p1 " )) * ((p2 * (p2 " )) * p1)
by RELAT_1:55
.=
(q * (p1 " )) * ((id (rng p2)) * p1)
by A12, FUNCT_1:61
.=
(q * (p1 " )) * p1
by A6, A9, RELAT_1:80
.=
q * ((p1 " ) * p1)
by RELAT_1:55
.=
q * (id (dom p1))
by A11, FUNCT_1:61
.=
q
by A15, RELAT_1:78
;
A19:
rng p2 = dom (p1 " )
by A6, A9, A11, FUNCT_1:55;
then A20:
rng ((p1 " ) * p2) =
rng (p1 " )
by RELAT_1:47
.=
dom q
by A11, A15, FUNCT_1:55
;
dom ((p1 " ) * p2) = dom p2
by A19, RELAT_1:46;
then A21:
dom (q * ((p1 " ) * p2)) = dom p2
by A20, RELAT_1:46;
A22:
Seg (len q1) =
dom q1
by FINSEQ_1:def 3
.=
dom p2
by A21, RELAT_1:55
.=
Seg (len p2)
by FINSEQ_1:def 3
;
then A23:
len q1 = len p2
by FINSEQ_1:8;
A24:
dom p2 =
Seg (len q1)
by A22, FINSEQ_1:def 3
.=
dom q1
by FINSEQ_1:def 3
;
A25:
rng p1 = dom (p2 " )
by A6, A9, A12, FUNCT_1:55;
then A26:
rng ((p2 " ) * p1) =
rng (p2 " )
by RELAT_1:47
.=
dom q1
by A12, A24, FUNCT_1:55
;
dom ((p2 " ) * p1) = dom p1
by A25, RELAT_1:46;
then A27:
dom (q1 * ((p2 " ) * p1)) = dom p1
by A26, RELAT_1:46;
A28:
rng (MergeSequence p1,q) c= rng (MergeSequence p2,q1)
proof
let z be
set ;
:: 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 A29:
j in dom (MergeSequence p1,q)
and A30:
(MergeSequence p1,q) . j = z
by FINSEQ_2:11;
j in Seg (len (MergeSequence p1,q))
by A29, FINSEQ_1:def 3;
then A31:
j in Seg (len p1)
by Def1;
then A32:
j in dom p1
by FINSEQ_1:def 3;
then A33:
j in dom ((p2 " ) * p1)
by A25, RELAT_1:46;
then
((p2 " ) * p1) . j in rng ((p2 " ) * p1)
by FUNCT_1:def 5;
then
((p2 " ) * p1) . j in rng (p2 " )
by FUNCT_1:25;
then A34:
((p2 " ) * p1) . j in dom p2
by A12, FUNCT_1:55;
then
((p2 " ) * p1) . j in Seg (len p2)
by FINSEQ_1:def 3;
then
((p2 " ) * p1) . j in Seg (len (MergeSequence p2,q1))
by Def1;
then A35:
((p2 " ) * p1) . j in dom (MergeSequence p2,q1)
by FINSEQ_1:def 3;
A36:
j in dom (q1 * ((p2 " ) * p1))
by A27, A31, FINSEQ_1:def 3;
A37:
q . j =
(q1 * ((p2 " ) * p1)) . j
by A18, RELAT_1:55
.=
q1 . (((p2 " ) * p1) . j)
by A36, FUNCT_1:22
;
reconsider pj =
((p2 " ) * p1) . j as
Element of
NAT by A34;
now per cases
( q . j = TRUE or not q . j = TRUE )
;
suppose
not
q . j = TRUE
;
:: thesis: (MergeSequence p2,q1) . (((p2 " ) * p1) . j) = zthen A39:
q . j = FALSE
by XBOOLEAN:def 3;
hence (MergeSequence p2,q1) . (((p2 " ) * p1) . j) =
X \ (p2 . pj)
by A34, A37, Th7
.=
X \ ((p2 * ((p2 " ) * p1)) . j)
by A33, FUNCT_1:23
.=
X \ (((p2 * (p2 " )) * p1) . j)
by RELAT_1:55
.=
X \ (((id (rng p1)) * p1) . j)
by A6, A9, A12, FUNCT_1:61
.=
X \ (p1 . j)
by RELAT_1:80
.=
z
by A30, A32, A39, Th7
;
:: thesis: verum end;
hence
z in rng (MergeSequence p2,q1)
by A35, FUNCT_1:def 5;
:: thesis: verum
end;
rng (MergeSequence p2,q1) c= rng (MergeSequence p1,q)
proof
let z be
set ;
:: 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:11;
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 p2
by FINSEQ_1:def 3;
then A44:
j in dom ((p1 " ) * p2)
by A19, RELAT_1:46;
then
((p1 " ) * p2) . j in rng ((p1 " ) * p2)
by FUNCT_1:def 5;
then
((p1 " ) * p2) . j in rng (p1 " )
by FUNCT_1:25;
then A45:
((p1 " ) * p2) . j in dom p1
by A11, FUNCT_1:55;
then
((p1 " ) * p2) . j in Seg (len p1)
by FINSEQ_1:def 3;
then
((p1 " ) * p2) . j in Seg (len (MergeSequence p1,q))
by Def1;
then A46:
((p1 " ) * p2) . j in dom (MergeSequence p1,q)
by FINSEQ_1:def 3;
A47:
j in dom (q * ((p1 " ) * p2))
by A21, A42, FINSEQ_1:def 3;
A48:
q1 . j =
(q * ((p1 " ) * p2)) . j
by RELAT_1:55
.=
q . (((p1 " ) * p2) . j)
by A47, FUNCT_1:22
;
reconsider pj =
((p1 " ) * p2) . j as
Element of
NAT by A45;
now per cases
( q1 . j = TRUE or not q1 . j = TRUE )
;
suppose
not
q1 . j = TRUE
;
:: thesis: (MergeSequence p1,q) . (((p1 " ) * p2) . j) = zthen A50:
q1 . j = FALSE
by XBOOLEAN:def 3;
hence (MergeSequence p1,q) . (((p1 " ) * p2) . j) =
X \ (p1 . pj)
by A45, A48, Th7
.=
X \ ((p1 * ((p1 " ) * p2)) . j)
by A44, FUNCT_1:23
.=
X \ (((p1 * (p1 " )) * p2) . j)
by RELAT_1:55
.=
X \ (((id (rng p2)) * p2) . j)
by A6, A9, A11, FUNCT_1:61
.=
X \ (p2 . j)
by RELAT_1:80
.=
z
by A41, A43, A50, Th7
;
:: thesis: verum end;
hence
z in rng (MergeSequence p1,q)
by A46, FUNCT_1:def 5;
:: thesis: verum
end;
then
P = Intersect (rng (MergeSequence p2,q1))
by A13, A28, XBOOLE_0:def 10;
hence
P in C2
by A10, A23;
:: thesis: verum
end; thus
(
P in C2 implies
P in C1 )
:: thesis: verumproof
assume
P in C2
;
:: thesis: P in C1
then consider q being
FinSequence of
BOOLEAN such that A51:
P = Intersect (rng (MergeSequence p2,q))
and A52:
len q = len p2
by A10;
A53:
dom p2 =
Seg (len q)
by A52, FINSEQ_1:def 3
.=
dom q
by FINSEQ_1:def 3
;
A54:
p1 is
FinSequence of
rng p2
by A6, A9, FINSEQ_1:def 4;
A55:
q is
Function of
(dom p2),
BOOLEAN
by A53, FINSEQ_2:30;
p2 is
Function of
(dom p2),
(rng p2)
by FUNCT_2:3;
then
p2 " is
Function of
(rng p2),
(dom p2)
by A12, FUNCT_2:31;
then
(p2 " ) * p1 is
FinSequence of
dom p2
by A54, FINSEQ_2:36;
then
q * ((p2 " ) * p1) is
FinSequence of
BOOLEAN
by A55, FINSEQ_2:36;
then reconsider q1 =
(q * (p2 " )) * p1 as
FinSequence of
BOOLEAN by RELAT_1:55;
A56:
(q1 * (p1 " )) * p2 =
((q * (p2 " )) * p1) * ((p1 " ) * p2)
by RELAT_1:55
.=
(q * (p2 " )) * (p1 * ((p1 " ) * p2))
by RELAT_1:55
.=
(q * (p2 " )) * ((p1 * (p1 " )) * p2)
by RELAT_1:55
.=
(q * (p2 " )) * ((id (rng p1)) * p2)
by A11, FUNCT_1:61
.=
(q * (p2 " )) * p2
by A6, A9, RELAT_1:80
.=
q * ((p2 " ) * p2)
by RELAT_1:55
.=
q * (id (dom p2))
by A12, FUNCT_1:61
.=
q
by A53, RELAT_1:78
;
A57:
rng p1 = dom (p2 " )
by A6, A9, A12, FUNCT_1:55;
then A58:
rng ((p2 " ) * p1) =
rng (p2 " )
by RELAT_1:47
.=
dom q
by A12, A53, FUNCT_1:55
;
dom ((p2 " ) * p1) = dom p1
by A57, RELAT_1:46;
then A59:
dom (q * ((p2 " ) * p1)) = dom p1
by A58, RELAT_1:46;
A60:
Seg (len q1) =
dom q1
by FINSEQ_1:def 3
.=
dom p1
by A59, RELAT_1:55
.=
Seg (len p1)
by FINSEQ_1:def 3
;
then A61:
len q1 = len p1
by FINSEQ_1:8;
A62:
dom p1 =
Seg (len q1)
by A60, FINSEQ_1:def 3
.=
dom q1
by FINSEQ_1:def 3
;
A63:
rng p2 = dom (p1 " )
by A6, A9, A11, FUNCT_1:55;
then A64:
rng ((p1 " ) * p2) =
rng (p1 " )
by RELAT_1:47
.=
dom q1
by A11, A62, FUNCT_1:55
;
dom ((p1 " ) * p2) = dom p2
by A63, RELAT_1:46;
then A65:
dom (q1 * ((p1 " ) * p2)) = dom p2
by A64, RELAT_1:46;
A66:
rng (MergeSequence p2,q) c= rng (MergeSequence p1,q1)
proof
let z be
set ;
:: 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 A67:
j in dom (MergeSequence p2,q)
and A68:
(MergeSequence p2,q) . j = z
by FINSEQ_2:11;
j in Seg (len (MergeSequence p2,q))
by A67, FINSEQ_1:def 3;
then A69:
j in Seg (len p2)
by Def1;
then A70:
j in dom p2
by FINSEQ_1:def 3;
then A71:
j in dom ((p1 " ) * p2)
by A63, RELAT_1:46;
then
((p1 " ) * p2) . j in rng ((p1 " ) * p2)
by FUNCT_1:def 5;
then
((p1 " ) * p2) . j in rng (p1 " )
by FUNCT_1:25;
then A72:
((p1 " ) * p2) . j in dom p1
by A11, FUNCT_1:55;
then
((p1 " ) * p2) . j in Seg (len p1)
by FINSEQ_1:def 3;
then
((p1 " ) * p2) . j in Seg (len (MergeSequence p1,q1))
by Def1;
then A73:
((p1 " ) * p2) . j in dom (MergeSequence p1,q1)
by FINSEQ_1:def 3;
A74:
j in dom (q1 * ((p1 " ) * p2))
by A65, A69, FINSEQ_1:def 3;
A75:
q . j =
(q1 * ((p1 " ) * p2)) . j
by A56, RELAT_1:55
.=
q1 . (((p1 " ) * p2) . j)
by A74, FUNCT_1:22
;
reconsider pj =
((p1 " ) * p2) . j as
Element of
NAT by A72;
now per cases
( q . j = TRUE or not q . j = TRUE )
;
suppose
not
q . j = TRUE
;
:: thesis: (MergeSequence p1,q1) . (((p1 " ) * p2) . j) = zthen A77:
q . j = FALSE
by XBOOLEAN:def 3;
hence (MergeSequence p1,q1) . (((p1 " ) * p2) . j) =
X \ (p1 . pj)
by A72, A75, Th7
.=
X \ ((p1 * ((p1 " ) * p2)) . j)
by A71, FUNCT_1:23
.=
X \ (((p1 * (p1 " )) * p2) . j)
by RELAT_1:55
.=
X \ (((id (rng p2)) * p2) . j)
by A6, A9, A11, FUNCT_1:61
.=
X \ (p2 . j)
by RELAT_1:80
.=
z
by A68, A70, A77, Th7
;
:: thesis: verum end;
hence
z in rng (MergeSequence p1,q1)
by A73, FUNCT_1:def 5;
:: thesis: verum
end;
rng (MergeSequence p1,q1) c= rng (MergeSequence p2,q)
proof
let z be
set ;
:: 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:11;
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 p1
by FINSEQ_1:def 3;
then A82:
j in dom ((p2 " ) * p1)
by A57, RELAT_1:46;
then
((p2 " ) * p1) . j in rng ((p2 " ) * p1)
by FUNCT_1:def 5;
then
((p2 " ) * p1) . j in rng (p2 " )
by FUNCT_1:25;
then A83:
((p2 " ) * p1) . j in dom p2
by A12, FUNCT_1:55;
then
((p2 " ) * p1) . j in Seg (len p2)
by FINSEQ_1:def 3;
then
((p2 " ) * p1) . j in Seg (len (MergeSequence p2,q))
by Def1;
then A84:
((p2 " ) * p1) . j in dom (MergeSequence p2,q)
by FINSEQ_1:def 3;
A85:
j in dom (q * ((p2 " ) * p1))
by A59, A80, FINSEQ_1:def 3;
A86:
q1 . j =
(q * ((p2 " ) * p1)) . j
by RELAT_1:55
.=
q . (((p2 " ) * p1) . j)
by A85, FUNCT_1:22
;
reconsider pj =
((p2 " ) * p1) . j as
Element of
NAT by A83;
now per cases
( q1 . j = TRUE or not q1 . j = TRUE )
;
suppose
not
q1 . j = TRUE
;
:: thesis: (MergeSequence p2,q) . (((p2 " ) * p1) . j) = zthen A88:
q1 . j = FALSE
by XBOOLEAN:def 3;
hence (MergeSequence p2,q) . (((p2 " ) * p1) . j) =
X \ (p2 . pj)
by A83, A86, Th7
.=
X \ ((p2 * ((p2 " ) * p1)) . j)
by A82, FUNCT_1:23
.=
X \ (((p2 * (p2 " )) * p1) . j)
by RELAT_1:55
.=
X \ (((id (rng p1)) * p1) . j)
by A6, A9, A12, FUNCT_1:61
.=
X \ (p1 . j)
by RELAT_1:80
.=
z
by A79, A81, A88, Th7
;
:: thesis: verum end;
hence
z in rng (MergeSequence p2,q)
by A84, FUNCT_1:def 5;
:: thesis: verum
end;
then
P = Intersect (rng (MergeSequence p1,q1))
by A51, A66, XBOOLE_0:def 10;
hence
P in C1
by A7, A61;
:: thesis: verum
end; end; hence
C1 = C2
by SETFAM_1:44;
:: thesis: verum end;
hence
C1 = C2
; :: thesis: verum