let X, Y be set ; for i, j being Nat st X c= Seg i & Y c= Seg j holds
( ( for m, n being Nat st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
let i, j be Nat; ( X c= Seg i & Y c= Seg j implies ( ( for m, n being Nat st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) ) )
assume that
A1:
X c= Seg i
and
A2:
Y c= Seg j
; ( ( for m, n being Nat st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
set r = Sgm (X \/ Y);
set q = Sgm Y;
set p = Sgm X;
Seg i, Seg j are_c=-comparable
by Th19;
then
( Seg i c= Seg j or Seg j c= Seg i )
;
then A3:
( X c= Seg j or Y c= Seg i )
by A1, A2;
then A4:
( X \/ Y c= Seg i or X \/ Y c= Seg j )
by A1, A2, XBOOLE_1:8;
thus
( ( for m, n being Nat st m in X & n in Y holds
m < n ) implies Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
( Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) implies for m, n being Nat st m in X & n in Y holds
m < n )proof
reconsider X1 =
X,
Y1 =
Y as
finite set by A1, A2;
defpred S1[
Nat]
means ( $1
in dom (Sgm X) implies
(Sgm (X \/ Y)) . $1
= (Sgm X) . $1 );
assume A5:
for
m,
n being
Nat st
m in X &
n in Y holds
m < n
;
Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
X /\ Y = {}
then A9:
X misses Y
;
A10:
len (Sgm (X \/ Y)) =
card (X1 \/ Y1)
by A1, A2, A3, Th37, XBOOLE_1:8
.=
(card X1) + (card Y1)
by A9, CARD_2:40
.=
(len (Sgm X)) + (card Y1)
by A1, Th37
.=
(len (Sgm X)) + (len (Sgm Y))
by A2, Th37
;
A11:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A12:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
assume A13:
k + 1
in dom (Sgm X)
;
(Sgm (X \/ Y)) . (k + 1) = (Sgm X) . (k + 1)
then A14:
(Sgm X) . (k + 1) in rng (Sgm X)
by FUNCT_1:def 3;
then reconsider n =
(Sgm X) . (k + 1) as
Element of
NAT ;
A15:
n in X
by A1, A14, FINSEQ_1:def 13;
len (Sgm X) <= len (Sgm (X \/ Y))
by A10, NAT_1:12;
then
Seg (len (Sgm X)) c= Seg (len (Sgm (X \/ Y)))
by FINSEQ_1:5;
then
dom (Sgm X) c= Seg (len (Sgm (X \/ Y)))
by FINSEQ_1:def 3;
then A16:
dom (Sgm X) c= dom (Sgm (X \/ Y))
by FINSEQ_1:def 3;
then A17:
(Sgm (X \/ Y)) . (k + 1) in rng (Sgm (X \/ Y))
by A13, FUNCT_1:def 3;
then reconsider m =
(Sgm (X \/ Y)) . (k + 1) as
Element of
NAT ;
A18:
m in X \/ Y
by A4, A17, FINSEQ_1:def 13;
assume A19:
(Sgm (X \/ Y)) . (k + 1) <> (Sgm X) . (k + 1)
;
contradiction
A20:
k + 1
in dom (Sgm (X \/ Y))
by A13, A16;
now contradictionper cases
( k in dom (Sgm X) or not k in dom (Sgm X) )
;
suppose A21:
k in dom (Sgm X)
;
contradictionthen
(Sgm X) . k in rng (Sgm X)
by FUNCT_1:def 3;
then reconsider n1 =
(Sgm X) . k as
Element of
NAT ;
(Sgm (X \/ Y)) . k in rng (Sgm (X \/ Y))
by A16, A21, FUNCT_1:def 3;
then reconsider m1 =
(Sgm (X \/ Y)) . k as
Element of
NAT ;
now contradictionper cases
( m < n or n < m )
by A19, XXREAL_0:1;
suppose A22:
m < n
;
contradictionA23:
1
<= k + 1
by A13, Th25;
not
m in Y
by A5, A15, A22;
then
m in X
by A18, XBOOLE_0:def 3;
then
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
object such that A24:
x in dom (Sgm X)
and A25:
(Sgm X) . x = m
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A24;
x <= len (Sgm X)
by A24, Th25;
then A26:
x < k + 1
by A1, A22, A25, A23, Th39;
k + 1
in Seg (len (Sgm (X \/ Y)))
by A20, FINSEQ_1:def 3;
then A27:
k + 1
<= len (Sgm (X \/ Y))
by FINSEQ_1:1;
k in Seg (len (Sgm X))
by A21, FINSEQ_1:def 3;
then A28:
1
<= k
by FINSEQ_1:1;
k < k + 1
by XREAL_1:29;
then A29:
n1 < m
by A4, A12, A21, A28, A27, FINSEQ_1:def 13;
A30:
k <= len (Sgm X)
by A21, Th25;
1
<= x
by A24, Th25;
then
k < x
by A1, A25, A29, A30, Th39;
hence
contradiction
by A26, NAT_1:13;
verum end; suppose A31:
n < m
;
contradictionA32:
1
<= k + 1
by A13, Th25;
n in X \/ Y
by A15, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
object such that A33:
x in dom (Sgm (X \/ Y))
and A34:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A33;
x <= len (Sgm (X \/ Y))
by A33, Th25;
then A35:
x < k + 1
by A1, A2, A3, A31, A34, A32, Th39, XBOOLE_1:8;
A36:
k + 1
<= len (Sgm X)
by A13, Th25;
A37:
k < k + 1
by XREAL_1:29;
1
<= k
by A21, Th25;
then A38:
m1 < n
by A1, A12, A21, A37, A36, FINSEQ_1:def 13;
A39:
k <= len (Sgm (X \/ Y))
by A16, A21, Th25;
1
<= x
by A33, Th25;
then
k < x
by A1, A2, A3, A34, A38, A39, Th39, XBOOLE_1:8;
hence
contradiction
by A35, NAT_1:13;
verum end; hence
contradiction
;
verum end; suppose A40:
not
k in dom (Sgm X)
;
contradictionA41:
k < k + 1
by XREAL_1:29;
(
k < 1 or
len (Sgm X) < k )
by A40, Th25;
then A42:
(
k = 0 or (
len (Sgm X) < k + 1 &
k + 1
<= len (Sgm X) ) )
by A13, A41, Th25, NAT_1:14, XXREAL_0:2;
now contradictionper cases
( m < n or n < m )
by A19, XXREAL_0:1;
suppose A43:
m < n
;
contradictionthen
not
m in Y
by A5, A15;
then
m in X
by A18, XBOOLE_0:def 3;
then
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
object such that A44:
x in dom (Sgm X)
and A45:
(Sgm X) . x = m
by FUNCT_1:def 3;
A46:
1
<= k + 1
by A13, Th25;
reconsider x =
x as
Element of
NAT by A44;
x <= len (Sgm X)
by A44, Th25;
then
x < k + 1
by A1, A43, A45, A46, Th39;
hence
contradiction
by A42, A44, Th24, NAT_1:14;
verum end; suppose A47:
n < m
;
contradictionA48:
1
<= k + 1
by A13, Th25;
n in X \/ Y
by A15, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
object such that A49:
x in dom (Sgm (X \/ Y))
and A50:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A49;
x <= len (Sgm (X \/ Y))
by A49, Th25;
then
x < k + 1
by A1, A2, A3, A47, A50, A48, Th39, XBOOLE_1:8;
hence
contradiction
by A42, A49, Th24, NAT_1:14;
verum end; hence
contradiction
;
verum end;
hence
contradiction
;
verum
end; end;
A51:
S1[
0 ]
by Th24;
A52:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A51, A11);
defpred S2[
Nat]
means ( $1
in dom (Sgm Y) implies
(Sgm (X \/ Y)) . ((len (Sgm X)) + $1) = (Sgm Y) . $1 );
A53:
now for k being Nat st S2[k] holds
S2[k + 1]let k be
Nat;
( S2[k] implies S2[k + 1] )assume A54:
S2[
k]
;
S2[k + 1]thus
S2[
k + 1]
verumproof
set a =
(len (Sgm X)) + (k + 1);
assume A55:
k + 1
in dom (Sgm Y)
;
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) = (Sgm Y) . (k + 1)
then
k + 1
<= len (Sgm Y)
by Th25;
then A56:
(len (Sgm X)) + (k + 1) <= len (Sgm (X \/ Y))
by A10, XREAL_1:7;
A57:
1
<= k + 1
by NAT_1:12;
then
1
<= (len (Sgm X)) + (k + 1)
by NAT_1:12;
then A58:
(len (Sgm X)) + (k + 1) in dom (Sgm (X \/ Y))
by A56, Th25;
then A59:
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) in rng (Sgm (X \/ Y))
by FUNCT_1:def 3;
reconsider m =
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) as
Element of
NAT by A59;
A60:
now not m in Xassume
m in X
;
contradictionthen
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
object such that A61:
x in dom (Sgm X)
and A62:
(Sgm X) . x = m
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A61;
x <= len (Sgm X)
by A61, Th25;
then A63:
x <= len (Sgm (X \/ Y))
by A10, NAT_1:12;
A64:
Sgm (X \/ Y) is
one-to-one
by A1, A2, A3, Lm1, XBOOLE_1:8;
1
<= x
by A61, Th25;
then A65:
x in dom (Sgm (X \/ Y))
by A63, Th25;
(Sgm (X \/ Y)) . x = (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1))
by A52, A61, A62;
then
x = (len (Sgm X)) + (k + 1)
by A58, A64, A65;
then
(len (Sgm X)) + (k + 1) <= (len (Sgm X)) + 0
by A61, Th25;
hence
contradiction
by XREAL_1:29;
verum end;
A66:
(Sgm Y) . (k + 1) in rng (Sgm Y)
by A55, FUNCT_1:def 3;
then reconsider n =
(Sgm Y) . (k + 1) as
Element of
NAT ;
A67:
n in Y
by A2, A66, FINSEQ_1:def 13;
assume A68:
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) <> (Sgm Y) . (k + 1)
;
contradiction
A69:
m in X \/ Y
by A4, A59, FINSEQ_1:def 13;
now contradictionper cases
( k in dom (Sgm Y) or not k in dom (Sgm Y) )
;
suppose A70:
k in dom (Sgm Y)
;
contradictionthen
(Sgm Y) . k in rng (Sgm Y)
by FUNCT_1:def 3;
then reconsider n1 =
(Sgm Y) . k as
Element of
NAT ;
1
<= k
by A70, Th25;
then A71:
1
<= (len (Sgm X)) + k
by NAT_1:12;
A72:
k <= len (Sgm Y)
by A70, Th25;
then
(len (Sgm X)) + k <= len (Sgm (X \/ Y))
by A10, XREAL_1:7;
then
(len (Sgm X)) + k in dom (Sgm (X \/ Y))
by A71, Th25;
then
(Sgm (X \/ Y)) . ((len (Sgm X)) + k) in rng (Sgm (X \/ Y))
by FUNCT_1:def 3;
then reconsider m1 =
(Sgm (X \/ Y)) . ((len (Sgm X)) + k) as
Element of
NAT ;
now contradictionper cases
( m < n or n < m )
by A68, XXREAL_0:1;
suppose A73:
m < n
;
contradictionA74:
1
<= k + 1
by A55, Th25;
m in Y
by A69, A60, XBOOLE_0:def 3;
then
m in rng (Sgm Y)
by A2, FINSEQ_1:def 13;
then consider x being
object such that A75:
x in dom (Sgm Y)
and A76:
(Sgm Y) . x = m
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A75;
x <= len (Sgm Y)
by A75, Th25;
then A77:
x < k + 1
by A2, A73, A76, A74, Th39;
(len (Sgm X)) + k < ((len (Sgm X)) + k) + 1
by XREAL_1:29;
then A78:
n1 < m
by A4, A54, A56, A70, A71, FINSEQ_1:def 13;
A79:
k <= len (Sgm Y)
by A70, Th25;
1
<= x
by A75, Th25;
then
k < x
by A2, A76, A78, A79, Th39;
hence
contradiction
by A77, NAT_1:13;
verum end; suppose A80:
n < m
;
contradictionA81:
1
<= (len (Sgm X)) + (k + 1)
by A57, NAT_1:12;
n in X \/ Y
by A67, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
object such that A82:
x in dom (Sgm (X \/ Y))
and A83:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A82;
x <= len (Sgm (X \/ Y))
by A82, Th25;
then A84:
x < ((len (Sgm X)) + k) + 1
by A1, A2, A3, A80, A83, A81, Th39, XBOOLE_1:8;
A85:
k + 1
<= len (Sgm Y)
by A55, Th25;
A86:
k < k + 1
by XREAL_1:29;
1
<= k
by A70, Th25;
then A87:
m1 < n
by A2, A54, A70, A86, A85, FINSEQ_1:def 13;
A88:
(len (Sgm X)) + k <= len (Sgm (X \/ Y))
by A10, A72, XREAL_1:7;
1
<= x
by A82, Th25;
then
(len (Sgm X)) + k < x
by A1, A2, A3, A83, A87, A88, Th39, XBOOLE_1:8;
hence
contradiction
by A84, NAT_1:13;
verum end; hence
contradiction
;
verum end; suppose A89:
not
k in dom (Sgm Y)
;
contradictionA90:
k < k + 1
by XREAL_1:29;
(
k < 1 or
len (Sgm Y) < k )
by A89, Th25;
then A91:
(
k = 0 or (
len (Sgm Y) < k + 1 &
k + 1
<= len (Sgm Y) ) )
by A55, A90, Th25, NAT_1:14, XXREAL_0:2;
now contradictionper cases
( m < n or n < m )
by A68, XXREAL_0:1;
suppose A92:
m < n
;
contradictionA93:
1
<= k + 1
by A55, Th25;
m in Y
by A69, A60, XBOOLE_0:def 3;
then
m in rng (Sgm Y)
by A2, FINSEQ_1:def 13;
then consider x being
object such that A94:
x in dom (Sgm Y)
and A95:
(Sgm Y) . x = m
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A94;
x <= len (Sgm Y)
by A94, Th25;
then
x < k + 1
by A2, A92, A95, A93, Th39;
hence
contradiction
by A91, A94, Th24, NAT_1:14;
verum end; suppose A96:
n < m
;
contradictionA97:
1
<= (len (Sgm X)) + 1
by NAT_1:12;
n in X \/ Y
by A67, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
object such that A98:
x in dom (Sgm (X \/ Y))
and A99:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A98;
x <= len (Sgm (X \/ Y))
by A98, Th25;
then
x < (len (Sgm X)) + 1
by A1, A2, A3, A91, A96, A99, A97, Th39, XBOOLE_1:8;
then A100:
x <= len (Sgm X)
by NAT_1:13;
1
<= x
by A98, Th25;
then A101:
x in dom (Sgm X)
by A100, Th25;
then A102:
(Sgm X) . x in rng (Sgm X)
by FUNCT_1:def 3;
n = (Sgm X) . x
by A52, A99, A101;
then
n in X
by A1, A102, FINSEQ_1:def 13;
hence
contradiction
by A5, A67;
verum end; hence
contradiction
;
verum end;
hence
contradiction
;
verum
end; end;
A103:
S2[
0 ]
by Th24;
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A103, A53);
hence
Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
by A10, A52, Th36;
verum
end;
assume A104:
Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
; for m, n being Nat st m in X & n in Y holds
m < n
let m, n be Nat; ( m in X & n in Y implies m < n )
assume that
A105:
m in X
and
A106:
n in Y
; m < n
n in rng (Sgm Y)
by A2, A106, FINSEQ_1:def 13;
then consider y being object such that
A107:
y in dom (Sgm Y)
and
A108:
(Sgm Y) . y = n
by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A107;
A109:
n = (Sgm (X \/ Y)) . ((len (Sgm X)) + y)
by A104, A107, A108, FINSEQ_1:def 7;
y <= len (Sgm Y)
by A107, Th25;
then
(len (Sgm X)) + y <= (len (Sgm X)) + (len (Sgm Y))
by XREAL_1:7;
then A110:
(len (Sgm X)) + y <= len (Sgm (X \/ Y))
by A104, FINSEQ_1:22;
m in rng (Sgm X)
by A1, A105, FINSEQ_1:def 13;
then consider x being object such that
A111:
x in dom (Sgm X)
and
A112:
(Sgm X) . x = m
by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A111;
A113:
x in Seg (len (Sgm X))
by A111, FINSEQ_1:def 3;
then A114:
1 <= x
by FINSEQ_1:1;
A115:
x <= len (Sgm X)
by A113, FINSEQ_1:1;
y <> 0
by A107, Th24;
then A116:
x < (len (Sgm X)) + y
by A115, NAT_1:16, XXREAL_0:2;
m = (Sgm (X \/ Y)) . x
by A104, A111, A112, FINSEQ_1:def 7;
hence
m < n
by A4, A109, A114, A116, A110, FINSEQ_1:def 13; verum