let X, Y be set ; for i, j being natural number st X c= Seg i & Y c= Seg j holds
( ( for m, n being Element of NAT st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
let i, j be natural number ; ( X c= Seg i & Y c= Seg j implies ( ( for m, n being Element of 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 Element of 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 Th20;
then
( Seg i c= Seg j or Seg j c= Seg i )
by XBOOLE_0:def 9;
then A3:
( X c= Seg j or Y c= Seg i )
by A1, A2, XBOOLE_1:1;
then A4:
( X \/ Y c= Seg i or X \/ Y c= Seg j )
by A1, A2, XBOOLE_1:8;
thus
( ( for m, n being Element of 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 Element of 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[
Element of
NAT ]
means ( $1
in dom (Sgm X) implies
(Sgm (X \/ Y)) . $1
= (Sgm X) . $1 );
assume A5:
for
m,
n being
Element of
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
by XBOOLE_0:def 7;
A10:
len (Sgm (X \/ Y)) =
card (X1 \/ Y1)
by A1, A2, A3, Th44, XBOOLE_1:8
.=
(card X1) + (card Y1)
by A9, CARD_2:53
.=
(len (Sgm X)) + (card Y1)
by A1, Th44
.=
(len (Sgm X)) + (len (Sgm Y))
by A2, Th44
;
A11:
now let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )assume A12:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
assume A15:
k + 1
in dom (Sgm X)
;
(Sgm (X \/ Y)) . (k + 1) = (Sgm X) . (k + 1)
then A16:
(Sgm X) . (k + 1) in rng (Sgm X)
by FUNCT_1:def 5;
then reconsider n =
(Sgm X) . (k + 1) as
Element of
NAT ;
A17:
n in X
by A1, A16, 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:7;
then
dom (Sgm X) c= Seg (len (Sgm (X \/ Y)))
by FINSEQ_1:def 3;
then A18:
dom (Sgm X) c= dom (Sgm (X \/ Y))
by FINSEQ_1:def 3;
then A19:
(Sgm (X \/ Y)) . (k + 1) in rng (Sgm (X \/ Y))
by A15, FUNCT_1:def 5;
then reconsider m =
(Sgm (X \/ Y)) . (k + 1) as
Element of
NAT ;
A20:
m in X \/ Y
by A4, A19, FINSEQ_1:def 13;
assume A21:
(Sgm (X \/ Y)) . (k + 1) <> (Sgm X) . (k + 1)
;
contradiction
A22:
k + 1
in dom (Sgm (X \/ Y))
by A15, A18;
now per cases
( k in dom (Sgm X) or not k in dom (Sgm X) )
;
suppose A23:
k in dom (Sgm X)
;
contradictionthen
(Sgm X) . k in rng (Sgm X)
by FUNCT_1:def 5;
then reconsider n1 =
(Sgm X) . k as
Element of
NAT ;
(Sgm (X \/ Y)) . k in rng (Sgm (X \/ Y))
by A18, A23, FUNCT_1:def 5;
then reconsider m1 =
(Sgm (X \/ Y)) . k as
Element of
NAT ;
now per cases
( m < n or n < m )
by A21, XXREAL_0:1;
suppose A24:
m < n
;
contradictionA25:
1
<= k + 1
by A15, Th27;
not
m in Y
by A5, A17, A24;
then
m in X
by A20, XBOOLE_0:def 3;
then
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
set such that A26:
x in dom (Sgm X)
and A27:
(Sgm X) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A26;
x <= len (Sgm X)
by A26, Th27;
then A28:
x < k + 1
by A1, A24, A27, A25, Th46;
k + 1
in Seg (len (Sgm (X \/ Y)))
by A22, FINSEQ_1:def 3;
then A29:
k + 1
<= len (Sgm (X \/ Y))
by FINSEQ_1:3;
k in Seg (len (Sgm X))
by A23, FINSEQ_1:def 3;
then A30:
1
<= k
by FINSEQ_1:3;
k < k + 1
by XREAL_1:31;
then A31:
n1 < m
by A4, A12, A23, A30, A29, FINSEQ_1:def 13;
A32:
k <= len (Sgm X)
by A23, Th27;
1
<= x
by A26, Th27;
then
k < x
by A1, A27, A31, A32, Th46;
hence
contradiction
by A28, NAT_1:13;
verum end; suppose A33:
n < m
;
contradictionA34:
1
<= k + 1
by A15, Th27;
n in X \/ Y
by A17, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A35:
x in dom (Sgm (X \/ Y))
and A36:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A35;
x <= len (Sgm (X \/ Y))
by A35, Th27;
then A37:
x < k + 1
by A1, A2, A3, A33, A36, A34, Th46, XBOOLE_1:8;
A38:
k + 1
<= len (Sgm X)
by A15, Th27;
A39:
k < k + 1
by XREAL_1:31;
1
<= k
by A23, Th27;
then A40:
m1 < n
by A1, A12, A23, A39, A38, FINSEQ_1:def 13;
A41:
k <= len (Sgm (X \/ Y))
by A18, A23, Th27;
1
<= x
by A35, Th27;
then
k < x
by A1, A2, A3, A36, A40, A41, Th46, XBOOLE_1:8;
hence
contradiction
by A37, NAT_1:13;
verum end; hence
contradiction
;
verum end; suppose A42:
not
k in dom (Sgm X)
;
contradictionA43:
k < k + 1
by XREAL_1:31;
(
k < 1 or
len (Sgm X) < k )
by A42, Th27;
then A44:
(
k = 0 or (
len (Sgm X) < k + 1 &
k + 1
<= len (Sgm X) ) )
by A15, A43, Th27, NAT_1:14, XXREAL_0:2;
now per cases
( m < n or n < m )
by A21, XXREAL_0:1;
suppose A45:
m < n
;
contradictionthen
not
m in Y
by A5, A17;
then
m in X
by A20, XBOOLE_0:def 3;
then
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
set such that A46:
x in dom (Sgm X)
and A47:
(Sgm X) . x = m
by FUNCT_1:def 5;
A48:
1
<= k + 1
by A15, Th27;
reconsider x =
x as
Element of
NAT by A46;
x <= len (Sgm X)
by A46, Th27;
then
x < k + 1
by A1, A45, A47, A48, Th46;
hence
contradiction
by A44, A46, Th26, NAT_1:14;
verum end; suppose A49:
n < m
;
contradictionA50:
1
<= k + 1
by A15, Th27;
n in X \/ Y
by A17, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A51:
x in dom (Sgm (X \/ Y))
and A52:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A51;
x <= len (Sgm (X \/ Y))
by A51, Th27;
then
x < k + 1
by A1, A2, A3, A49, A52, A50, Th46, XBOOLE_1:8;
hence
contradiction
by A44, A51, Th26, NAT_1:14;
verum end; hence
contradiction
;
verum end;
hence
contradiction
;
verum
end; end;
A53:
S1[
0 ]
by Th26;
A54:
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A53, A11);
defpred S2[
Element of
NAT ]
means ( $1
in dom (Sgm Y) implies
(Sgm (X \/ Y)) . ((len (Sgm X)) + $1) = (Sgm Y) . $1 );
A55:
now let k be
Element of
NAT ;
( S2[k] implies S2[k + 1] )assume A56:
S2[
k]
;
S2[k + 1]thus
S2[
k + 1]
verumproof
set a =
(len (Sgm X)) + (k + 1);
assume A58:
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 Th27;
then A59:
(len (Sgm X)) + (k + 1) <= len (Sgm (X \/ Y))
by A10, XREAL_1:9;
A60:
1
<= k + 1
by NAT_1:12;
then
1
<= (len (Sgm X)) + (k + 1)
by NAT_1:12;
then A61:
(len (Sgm X)) + (k + 1) in dom (Sgm (X \/ Y))
by A59, Th27;
then A62:
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) in rng (Sgm (X \/ Y))
by FUNCT_1:def 5;
reconsider m =
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) as
Element of
NAT by A62;
A64:
now assume
m in X
;
contradictionthen
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
set such that A65:
x in dom (Sgm X)
and A66:
(Sgm X) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A65;
x <= len (Sgm X)
by A65, Th27;
then A67:
x <= len (Sgm (X \/ Y))
by A10, NAT_1:12;
A68:
Sgm (X \/ Y) is
one-to-one
by A1, A2, A3, Lm1, XBOOLE_1:8;
1
<= x
by A65, Th27;
then A69:
x in dom (Sgm (X \/ Y))
by A67, Th27;
(Sgm (X \/ Y)) . x = (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1))
by A54, A65, A66;
then
x = (len (Sgm X)) + (k + 1)
by A61, A68, A69, FUNCT_1:def 8;
then
(len (Sgm X)) + (k + 1) <= (len (Sgm X)) + 0
by A65, Th27;
hence
contradiction
by XREAL_1:31;
verum end;
A70:
(Sgm Y) . (k + 1) in rng (Sgm Y)
by A58, FUNCT_1:def 5;
then reconsider n =
(Sgm Y) . (k + 1) as
Element of
NAT ;
A71:
n in Y
by A2, A70, FINSEQ_1:def 13;
assume A72:
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) <> (Sgm Y) . (k + 1)
;
contradiction
A73:
m in X \/ Y
by A4, A62, FINSEQ_1:def 13;
now per cases
( k in dom (Sgm Y) or not k in dom (Sgm Y) )
;
suppose A74:
k in dom (Sgm Y)
;
contradictionthen
(Sgm Y) . k in rng (Sgm Y)
by FUNCT_1:def 5;
then reconsider n1 =
(Sgm Y) . k as
Element of
NAT ;
1
<= k
by A74, Th27;
then A75:
1
<= (len (Sgm X)) + k
by NAT_1:12;
A76:
k <= len (Sgm Y)
by A74, Th27;
then
(len (Sgm X)) + k <= len (Sgm (X \/ Y))
by A10, XREAL_1:9;
then
(len (Sgm X)) + k in dom (Sgm (X \/ Y))
by A75, Th27;
then
(Sgm (X \/ Y)) . ((len (Sgm X)) + k) in rng (Sgm (X \/ Y))
by FUNCT_1:def 5;
then reconsider m1 =
(Sgm (X \/ Y)) . ((len (Sgm X)) + k) as
Element of
NAT ;
now per cases
( m < n or n < m )
by A72, XXREAL_0:1;
suppose A77:
m < n
;
contradictionA78:
1
<= k + 1
by A58, Th27;
m in Y
by A73, A64, XBOOLE_0:def 3;
then
m in rng (Sgm Y)
by A2, FINSEQ_1:def 13;
then consider x being
set such that A79:
x in dom (Sgm Y)
and A80:
(Sgm Y) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A79;
x <= len (Sgm Y)
by A79, Th27;
then A81:
x < k + 1
by A2, A77, A80, A78, Th46;
(len (Sgm X)) + k < ((len (Sgm X)) + k) + 1
by XREAL_1:31;
then A82:
n1 < m
by A4, A56, A59, A74, A75, FINSEQ_1:def 13;
A83:
k <= len (Sgm Y)
by A74, Th27;
1
<= x
by A79, Th27;
then
k < x
by A2, A80, A82, A83, Th46;
hence
contradiction
by A81, NAT_1:13;
verum end; suppose A84:
n < m
;
contradictionA85:
1
<= (len (Sgm X)) + (k + 1)
by A60, NAT_1:12;
n in X \/ Y
by A71, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A86:
x in dom (Sgm (X \/ Y))
and A87:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A86;
x <= len (Sgm (X \/ Y))
by A86, Th27;
then A88:
x < ((len (Sgm X)) + k) + 1
by A1, A2, A3, A84, A87, A85, Th46, XBOOLE_1:8;
A89:
k + 1
<= len (Sgm Y)
by A58, Th27;
A90:
k < k + 1
by XREAL_1:31;
1
<= k
by A74, Th27;
then A91:
m1 < n
by A2, A56, A74, A90, A89, FINSEQ_1:def 13;
A92:
(len (Sgm X)) + k <= len (Sgm (X \/ Y))
by A10, A76, XREAL_1:9;
1
<= x
by A86, Th27;
then
(len (Sgm X)) + k < x
by A1, A2, A3, A87, A91, A92, Th46, XBOOLE_1:8;
hence
contradiction
by A88, NAT_1:13;
verum end; hence
contradiction
;
verum end; suppose A93:
not
k in dom (Sgm Y)
;
contradictionA94:
k < k + 1
by XREAL_1:31;
(
k < 1 or
len (Sgm Y) < k )
by A93, Th27;
then A95:
(
k = 0 or (
len (Sgm Y) < k + 1 &
k + 1
<= len (Sgm Y) ) )
by A58, A94, Th27, NAT_1:14, XXREAL_0:2;
now per cases
( m < n or n < m )
by A72, XXREAL_0:1;
suppose A96:
m < n
;
contradictionA97:
1
<= k + 1
by A58, Th27;
m in Y
by A73, A64, XBOOLE_0:def 3;
then
m in rng (Sgm Y)
by A2, FINSEQ_1:def 13;
then consider x being
set such that A98:
x in dom (Sgm Y)
and A99:
(Sgm Y) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A98;
x <= len (Sgm Y)
by A98, Th27;
then
x < k + 1
by A2, A96, A99, A97, Th46;
hence
contradiction
by A95, A98, Th26, NAT_1:14;
verum end; suppose A100:
n < m
;
contradictionA101:
1
<= (len (Sgm X)) + 1
by NAT_1:12;
n in X \/ Y
by A71, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A102:
x in dom (Sgm (X \/ Y))
and A103:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A102;
x <= len (Sgm (X \/ Y))
by A102, Th27;
then
x < (len (Sgm X)) + 1
by A1, A2, A3, A95, A100, A103, A101, Th46, XBOOLE_1:8;
then A104:
x <= len (Sgm X)
by NAT_1:13;
1
<= x
by A102, Th27;
then A105:
x in dom (Sgm X)
by A104, Th27;
then A106:
(Sgm X) . x in rng (Sgm X)
by FUNCT_1:def 5;
n = (Sgm X) . x
by A54, A103, A105;
then
n in X
by A1, A106, FINSEQ_1:def 13;
hence
contradiction
by A5, A71;
verum end; hence
contradiction
;
verum end;
hence
contradiction
;
verum
end; end;
A107:
S2[
0 ]
by Th26;
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A107, A55);
hence
Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
by A10, A54, Th43;
verum
end;
assume A108:
Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
; for m, n being Element of NAT st m in X & n in Y holds
m < n
let m, n be Element of NAT ; ( m in X & n in Y implies m < n )
assume that
A109:
m in X
and
A110:
n in Y
; m < n
n in rng (Sgm Y)
by A2, A110, FINSEQ_1:def 13;
then consider y being set such that
A111:
y in dom (Sgm Y)
and
A112:
(Sgm Y) . y = n
by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A111;
A113:
n = (Sgm (X \/ Y)) . ((len (Sgm X)) + y)
by A108, A111, A112, FINSEQ_1:def 7;
y <= len (Sgm Y)
by A111, Th27;
then
(len (Sgm X)) + y <= (len (Sgm X)) + (len (Sgm Y))
by XREAL_1:9;
then A114:
(len (Sgm X)) + y <= len (Sgm (X \/ Y))
by A108, FINSEQ_1:35;
m in rng (Sgm X)
by A1, A109, FINSEQ_1:def 13;
then consider x being set such that
A115:
x in dom (Sgm X)
and
A116:
(Sgm X) . x = m
by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A115;
A117:
x in Seg (len (Sgm X))
by A115, FINSEQ_1:def 3;
then A118:
1 <= x
by FINSEQ_1:3;
A119:
x <= len (Sgm X)
by A117, FINSEQ_1:3;
y <> 0
by A111, Th26;
then A120:
x < (len (Sgm X)) + y
by A119, NAT_1:16, XXREAL_0:2;
m = (Sgm (X \/ Y)) . x
by A108, A115, A116, FINSEQ_1:def 7;
hence
m < n
by A4, A113, A118, A120, A114, FINSEQ_1:def 13; verum