begin
theorem
for
k,
n being
Nat holds
(
k - n in Seg k iff
n < k )
theorem Th20:
for
y being
set for
k being
Nat st
Seg k = {y} holds
(
k = 1 &
y = 1 )
Lm1:
for A being set
for k being Nat st A c= Seg k holds
Sgm A is one-to-one
Lm2:
for k being Nat holds (Sgm (Seg (k + 0))) | (Seg k) = Sgm (Seg k)
Lm3:
now for n being Nat st ( for k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ) holds
for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)
let n be
Nat;
( ( for k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ) implies for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k) )assume A1:
for
k being
Nat holds
(Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k)
;
for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)let k be
Nat;
(Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)set X =
Sgm (Seg (k + (n + 1)));
set Y =
Sgm (Seg (k + 1));
A2:
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)
proof
reconsider p =
(Sgm (Seg (k + 1))) | (Seg k) as
FinSequence of
NAT by FINSEQ_1:18;
A3:
len (Sgm (Seg (k + 1))) = k + 1
by Th46;
then A4:
dom (Sgm (Seg (k + 1))) = Seg (k + 1)
by FINSEQ_1:def 3;
A5:
k <= k + 1
by NAT_1:12;
then A6:
dom p = Seg k
by A3, FINSEQ_1:17;
A7:
rng (Sgm (Seg (k + 1))) = Seg (k + 1)
by FINSEQ_1:def 13;
A8:
(Sgm (Seg (k + 1))) . (k + 1) = k + 1
proof
k + 1
in dom (Sgm (Seg (k + 1)))
by A4, FINSEQ_1:4;
then A9:
(Sgm (Seg (k + 1))) . (k + 1) in Seg (k + 1)
by A7, FUNCT_1:def 3;
then reconsider n =
(Sgm (Seg (k + 1))) . (k + 1) as
Element of
NAT ;
A10:
k < k + 1
by XREAL_1:29;
k + 1
in rng (Sgm (Seg (k + 1)))
by A7, FINSEQ_1:4;
then consider x being
set such that A11:
x in dom (Sgm (Seg (k + 1)))
and A12:
(Sgm (Seg (k + 1))) . x = k + 1
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A11;
assume
not
(Sgm (Seg (k + 1))) . (k + 1) = k + 1
;
contradiction
then
not
(Sgm (Seg (k + 1))) . (k + 1) in {(k + 1)}
by TARSKI:def 1;
then
(Sgm (Seg (k + 1))) . (k + 1) in (Seg (k + 1)) \ {(k + 1)}
by A9, XBOOLE_0:def 5;
then A13:
(Sgm (Seg (k + 1))) . (k + 1) in Seg k
by FINSEQ_1:10;
A14:
now not x = k + 1
end;
x <= k + 1
by A3, A11, Th25;
then A16:
x < k + 1
by A14, XXREAL_0:1;
1
<= x
by A11, Th25;
then A17:
k + 1
< n
by A3, A12, A16, FINSEQ_1:def 13;
n <= k
by A13, FINSEQ_1:1;
hence
contradiction
by A17, A10, XXREAL_0:2;
verum
end;
A18:
Sgm (Seg (k + 1)) is
one-to-one
by Lm1;
rng p = (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
proof
thus
rng p c= (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
XBOOLE_0:def 10 (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} c= rng p
proof
let x be
set ;
TARSKI:def 3 ( not x in rng p or x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} )
assume A19:
x in rng p
;
x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
A20:
now not x in {(k + 1)}
assume
x in {(k + 1)}
;
contradictionthen A21:
x = k + 1
by TARSKI:def 1;
A22:
k < k + 1
by XREAL_1:29;
A23:
k + 1
in dom (Sgm (Seg (k + 1)))
by A4, FINSEQ_1:4;
A24:
Seg k c= Seg (k + 1)
by Th18;
consider y being
set such that A25:
y in dom p
and A26:
p . y = x
by A19, FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A25;
A27:
(Sgm (Seg (k + 1))) . y = p . y
by A25, FUNCT_1:47;
y <= k
by A6, A25, FINSEQ_1:1;
hence
contradiction
by A18, A4, A6, A8, A25, A26, A24, A27, A21, A23, A22, FUNCT_1:def 4;
verum
end;
rng p c= rng (Sgm (Seg (k + 1)))
by RELAT_1:70;
hence
x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
by A8, A19, A20, XBOOLE_0:def 5;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} or x in rng p )
assume A28:
x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
;
x in rng p
then
x in rng (Sgm (Seg (k + 1)))
by XBOOLE_0:def 5;
then consider y being
set such that A29:
y in dom (Sgm (Seg (k + 1)))
and A30:
(Sgm (Seg (k + 1))) . y = x
by FUNCT_1:def 3;
then
y in (Seg (k + 1)) \ {(k + 1)}
by A4, A29, XBOOLE_0:def 5;
then A32:
y in dom p
by A6, FINSEQ_1:10;
then
p . y = (Sgm (Seg (k + 1))) . y
by FUNCT_1:47;
hence
x in rng p
by A30, A32, FUNCT_1:def 3;
verum
end;
then A33:
rng p = Seg k
by A7, A8, FINSEQ_1:10;
now for i, j, l, m being Nat st 1 <= i & i < j & j <= len p & l = p . i & m = p . j holds
l < m
A34:
len p = k
by A3, A5, FINSEQ_1:17;
let i,
j,
l,
m be
Nat;
( 1 <= i & i < j & j <= len p & l = p . i & m = p . j implies l < m )assume that A35:
1
<= i
and A36:
i < j
and A37:
j <= len p
and A38:
l = p . i
and A39:
m = p . j
;
l < m
i <= len p
by A36, A37, XXREAL_0:2;
then
i in dom p
by A6, A35, A34, FINSEQ_1:1;
then A40:
p . i = (Sgm (Seg (k + 1))) . i
by FUNCT_1:47;
1
<= j
by A35, A36, XXREAL_0:2;
then
j in dom p
by A6, A37, A34, FINSEQ_1:1;
then A41:
p . j = (Sgm (Seg (k + 1))) . j
by FUNCT_1:47;
len (Sgm (Seg (k + 1))) = k + 1
by Th46;
then
j <= len (Sgm (Seg (k + 1)))
by A37, A34, NAT_1:12;
hence
l < m
by A35, A36, A38, A39, A40, A41, FINSEQ_1:def 13;
verum
end;
hence
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)
by A33, FINSEQ_1:def 13;
verum
end;
Sgm (Seg (k + (n + 1))) = Sgm (Seg ((k + 1) + n))
;
then
(Sgm (Seg (k + (n + 1)))) | (Seg (k + 1)) = Sgm (Seg (k + 1))
by A1;
then
Sgm (Seg k) = (Sgm (Seg (k + (n + 1)))) | ((Seg (k + 1)) /\ (Seg k))
by A2, RELAT_1:71;
hence
(Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)
by FINSEQ_1:7, NAT_1:12;
verum
end;
Lm4:
for n, k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k)
Lm5:
now for k being Nat st Sgm (Seg k) = idseq k holds
Sgm (Seg (k + 1)) = idseq (k + 1)
let k be
Nat;
( Sgm (Seg k) = idseq k implies Sgm (Seg (k + 1)) = idseq (k + 1) )assume A1:
Sgm (Seg k) = idseq k
;
Sgm (Seg (k + 1)) = idseq (k + 1)A2:
len (idseq (k + 1)) = k + 1
by CARD_1:def 7;
then A3:
len (Sgm (Seg (k + 1))) = len (idseq (k + 1))
by Th46;
then A4:
dom (Sgm (Seg (k + 1))) = Seg (k + 1)
by A2, FINSEQ_1:def 3;
now for j being Nat st j in dom (Sgm (Seg (k + 1))) holds
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
let j be
Nat;
( j in dom (Sgm (Seg (k + 1))) implies (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j )assume A5:
j in dom (Sgm (Seg (k + 1)))
;
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . jthen A6:
j in (Seg k) \/ {(k + 1)}
by A4, FINSEQ_1:9;
now (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
per cases
( j in Seg k or j in {(k + 1)} )
by A6, XBOOLE_0:def 3;
suppose A10:
j in {(k + 1)}
;
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
set Y =
Sgm (Seg k);
set X =
Sgm (Seg (k + 1));
A11:
j = k + 1
by A10, TARSKI:def 1;
then A12:
j in Seg (k + 1)
by FINSEQ_1:4;
now not (Sgm (Seg (k + 1))) . j <> j
rng (Sgm (Seg (k + 1))) = Seg (k + 1)
by FINSEQ_1:def 13;
then A13:
(Sgm (Seg (k + 1))) . j in Seg (k + 1)
by A5, FUNCT_1:def 3;
then reconsider n =
(Sgm (Seg (k + 1))) . j as
Element of
NAT ;
assume
(Sgm (Seg (k + 1))) . j <> j
;
contradictionthen
not
(Sgm (Seg (k + 1))) . j in {j}
by TARSKI:def 1;
then
(Sgm (Seg (k + 1))) . j in (Seg (k + 1)) \ {(k + 1)}
by A11, A13, XBOOLE_0:def 5;
then A14:
(Sgm (Seg (k + 1))) . j in Seg k
by FINSEQ_1:10;
A15:
Sgm (Seg (k + 1)) is
one-to-one
by Lm1;
A16:
dom (Sgm (Seg (k + 1))) = Seg (k + 1)
by A2, A3, FINSEQ_1:def 3;
A17:
k < k + 1
by XREAL_1:29;
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)
by Lm4;
then A18:
(Sgm (Seg (k + 1))) . n =
(Sgm (Seg k)) . n
by A14, FUNCT_1:49
.=
n
by A1, A14, FUNCT_1:18
;
n <= k
by A14, FINSEQ_1:1;
hence
contradiction
by A11, A12, A16, A13, A15, A18, A17, FUNCT_1:def 4;
verum
end;
hence
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
by A11, FINSEQ_1:4, FUNCT_1:18;
verum
end;
end;
end;
hence
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
;
verum
end;
hence
Sgm (Seg (k + 1)) = idseq (k + 1)
by A3, FINSEQ_2:9;
verum
end;
Lm6:
for x, A being set holds
( <*x*> - A = <*x*> iff not x in A )
Lm7:
for x, A being set holds
( <*x*> - A = {} iff x in A )
Lm8:
for p being FinSequence
for A being set holds (p ^ {}) - A = (p - A) ^ ({} - A)
Lm9:
for p being FinSequence
for x, A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
Lm11:
for q, p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A)
theorem
for
x,
y,
A being
set holds
(
<*x,y*> - A = <*x,y*> iff ( not
x in A & not
y in A ) )
Lm12:
for l being Nat st ( for p being FinSequence
for A being set st len p = l holds
for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) ) holds
for p being FinSequence
for A being set st len p = l + 1 holds
for n being Nat st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )
Lm13:
for l being Nat
for p being FinSequence
for A being set st len p = l holds
for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n )
begin
begin
definition
let D be non
empty set ;
let R be
Relation of
D;
existence
ex b1 being Relation of (D *) st
for x, y being FinSequence of D holds
( [x,y] in b1 iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) )
uniqueness
for b1, b2 being Relation of (D *) st ( for x, y being FinSequence of D holds
( [x,y] in b1 iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ) & ( for x, y being FinSequence of D holds
( [x,y] in b2 iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ) holds
b1 = b2
end;
theorem
for
f,
g,
h being
Function holds
(
doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> &
rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> )
:: proved in RLVECT_1 and has a number 104.