:: by Wojciech A. Trybulec

::

:: Received April 8, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem :: FINSEQ_3:23

theorem :: FINSEQ_3:26

for p being FinSequence

for n being Nat holds

( n in dom p iff ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) )

for n being Nat holds

( n in dom p iff ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) )

proof end;

theorem Th38: :: FINSEQ_3:38

for r, p, q being FinSequence st len r = (len p) + (len q) & ( for k being Element of NAT st k in dom p holds

r . k = p . k ) & ( for k being Element of NAT st k in dom q holds

r . ((len p) + k) = q . k ) holds

r = p ^ q

r . k = p . k ) & ( for k being Element of NAT st k in dom q holds

r . ((len p) + k) = q . k ) holds

r = p ^ q

proof end;

Lm1: for A being set

for k being Nat st A c= Seg k holds

Sgm A is one-to-one

proof end;

theorem Th41: :: FINSEQ_3:41

for X being set

for i, k, l, n, m being Nat st X c= Seg i & k < l & 1 <= n & m <= len (Sgm X) & (Sgm X) . m = k & (Sgm X) . n = l holds

m < n

for i, k, l, n, m being Nat st X c= Seg i & k < l & 1 <= n & m <= len (Sgm X) & (Sgm X) . m = k & (Sgm X) . n = l holds

m < n

proof end;

theorem Th42: :: FINSEQ_3:42

for X, Y being set

for i, j being Nat 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) )

for i, j being Nat 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) )

proof end;

:: The other way of the one above - FINSEQ_1:72.

Lm2: for k being Nat holds (Sgm (Seg (k + 0))) | (Seg k) = Sgm (Seg k)

proof end;

Lm3: now :: thesis: 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)

for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)

let n be Nat; :: thesis: ( ( 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) ; :: thesis: for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)

let k be Nat; :: thesis: (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)

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; :: thesis: verum

end;
assume A1: for k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ; :: thesis: for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)

let k be Nat; :: thesis: (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

Sgm (Seg (k + (n + 1))) = Sgm (Seg ((k + 1) + n))
;
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

rng p = (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}

end;
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

A18:
Sgm (Seg (k + 1)) is one-to-one
by Lm1;
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 ; :: thesis: 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;

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; :: thesis: verum

end;
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 ; :: thesis: 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 :: thesis: not x = k + 1

x <= k + 1
by A3, A11, Th25;
assume A15:
x = k + 1
; :: thesis: contradiction

n <= k by A13, FINSEQ_1:1;

hence contradiction by A12, A15, XREAL_1:29; :: thesis: verum

end;
n <= k by A13, FINSEQ_1:1;

hence contradiction by A12, A15, XREAL_1:29; :: thesis: verum

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; :: thesis: verum

rng p = (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}

proof

then A33:
rng p = Seg k
by A7, A8, FINSEQ_1:10;
thus
rng p c= (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
:: according to XBOOLE_0:def 10 :: thesis: (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} c= rng p

assume A28: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} ; :: thesis: 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 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; :: thesis: verum

end;
proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} or x in rng p )
let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}

hence x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} by A8, A19, A20, XBOOLE_0:def 5; :: thesis: verum

end;
assume A19: x in rng p ; :: thesis: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}

A20: now :: thesis: not x in {(k + 1)}

rng p c= rng (Sgm (Seg (k + 1)))
by RELAT_1:70;
assume
x in {(k + 1)}
; :: thesis: contradiction

then 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; :: thesis: verum

end;
then 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; :: thesis: verum

hence x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} by A8, A19, A20, XBOOLE_0:def 5; :: thesis: verum

assume A28: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} ; :: thesis: 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;

now :: thesis: not y in {(k + 1)}

then
y in (Seg (k + 1)) \ {(k + 1)}
by A4, A29, XBOOLE_0:def 5;
assume
y in {(k + 1)}
; :: thesis: contradiction

then A31: x = k + 1 by A8, A30, TARSKI:def 1;

not x in {(k + 1)} by A8, A28, XBOOLE_0:def 5;

hence contradiction by A31, TARSKI:def 1; :: thesis: verum

end;
then A31: x = k + 1 by A8, A30, TARSKI:def 1;

not x in {(k + 1)} by A8, A28, XBOOLE_0:def 5;

hence contradiction by A31, TARSKI:def 1; :: thesis: verum

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; :: thesis: verum

now :: thesis: for i, j, l, m being Nat st 1 <= i & i < j & j <= len p & l = p . i & m = p . j holds

l < m

hence
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)
by A33, FINSEQ_1:def 13; :: thesis: veruml < m

A34:
len p = k
by A3, A5, FINSEQ_1:17;

let i, j, l, m be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;
let i, j, l, m be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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; :: thesis: verum

Lm4: for n, k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k)

proof end;

Lm5: now :: thesis: for k being Nat st Sgm (Seg k) = idseq k holds

Sgm (Seg (k + 1)) = idseq (k + 1)

Sgm (Seg (k + 1)) = idseq (k + 1)

let k be Nat; :: thesis: ( Sgm (Seg k) = idseq k implies Sgm (Seg (k + 1)) = idseq (k + 1) )

assume A1: Sgm (Seg k) = idseq k ; :: thesis: 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;

end;
assume A1: Sgm (Seg k) = idseq k ; :: thesis: 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 :: thesis: for j being Nat st j in dom (Sgm (Seg (k + 1))) holds

(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j

hence
Sgm (Seg (k + 1)) = idseq (k + 1)
by A3, FINSEQ_2:9; :: thesis: verum(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j

let j be Nat; :: thesis: ( 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))) ; :: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j

then A6: j in (Seg k) \/ {(k + 1)} by A4, FINSEQ_1:9;

end;
assume A5: j in dom (Sgm (Seg (k + 1))) ; :: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j

then A6: j in (Seg k) \/ {(k + 1)} by A4, FINSEQ_1:9;

now :: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
end;

hence
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
; :: thesis: verum
per cases
( j in Seg k or j in {(k + 1)} )
by A6, XBOOLE_0:def 3;

end;

suppose A7:
j in Seg k
; :: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j

A8:
(idseq (k + 1)) . j = j
by A4, A5, FUNCT_1:18;

A9: (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by Lm4;

(Sgm (Seg k)) . j = j by A1, A7, FUNCT_1:18;

hence (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A7, A8, A9, FUNCT_1:49; :: thesis: verum

end;
A9: (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by Lm4;

(Sgm (Seg k)) . j = j by A1, A7, FUNCT_1:18;

hence (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A7, A8, A9, FUNCT_1:49; :: thesis: verum

suppose A10:
j in {(k + 1)}
; :: thesis: (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;

end;
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 :: thesis: not (Sgm (Seg (k + 1))) . j <> j

hence
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
by A11, FINSEQ_1:4, FUNCT_1:18; :: thesis: verum
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 ; :: thesis: contradiction

then 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; :: thesis: verum

end;
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 ; :: thesis: contradiction

then 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; :: thesis: verum

theorem :: FINSEQ_3:54

for p, q being FinSequence

for k, l being Nat st len p = k + l & q = p | (Seg k) holds

dom q = Seg k

for k, l being Nat st len p = k + l & q = p | (Seg k) holds

dom q = Seg k

proof end;

theorem Th55: :: FINSEQ_3:55

for p, q being FinSequence

for k being Nat st len p = k + 1 & q = p | (Seg k) holds

p = q ^ <*(p . (k + 1))*>

for k being Nat st len p = k + 1 & q = p | (Seg k) holds

p = q ^ <*(p . (k + 1))*>

proof end;

theorem :: FINSEQ_3:56

for p being FinSequence

for X being set holds

( p | X is FinSequence iff ex k being Element of NAT st X /\ (dom p) = Seg k )

for X being set holds

( p | X is FinSequence iff ex k being Element of NAT st X /\ (dom p) = Seg k )

proof end;

theorem Th57: :: FINSEQ_3:57

for p, q being FinSequence

for A being set holds card ((p ^ q) " A) = (card (p " A)) + (card (q " A))

for A being set holds card ((p ^ q) " A) = (card (p " A)) + (card (q " A))

proof end;

definition

let p be FinSequence;

let A be set ;

coherence

p * (Sgm ((dom p) \ (p " A))) is FinSequence

end;
let A be set ;

coherence

p * (Sgm ((dom p) \ (p " A))) is FinSequence

proof end;

:: deftheorem defines - FINSEQ_3:def 1 :

for p being FinSequence

for A being set holds p - A = p * (Sgm ((dom p) \ (p " A)));

for p being FinSequence

for A being set holds p - A = p * (Sgm ((dom p) \ (p " A)));

theorem :: FINSEQ_3:62

for p being FinSequence

for A being set

for n being Nat st n = (len p) - (card (p " A)) holds

dom (p - A) = Seg n

for A being set

for n being Nat st n = (len p) - (card (p " A)) holds

dom (p - A) = Seg n

proof end;

Lm6: for x, A being set holds

( <*x*> - A = <*x*> iff not x in A )

proof end;

Lm7: for x, A being set holds

( <*x*> - A = {} iff x in A )

proof end;

Lm8: for p being FinSequence

for A being set holds (p ^ {}) - A = (p - A) ^ ({} - A)

proof end;

Lm9: for p being FinSequence

for x, A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)

proof end;

Lm10: now :: thesis: for q being FinSequence

for x being set st ( for p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) holds

for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

for x being set st ( for p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) holds

for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

let q be FinSequence; :: thesis: for x being set st ( for p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) holds

for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

let x be set ; :: thesis: ( ( for p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) implies for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A) )

assume A1: for p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ; :: thesis: for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

let p be FinSequence; :: thesis: for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

let A be set ; :: thesis: (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

thus (p ^ (q ^ <*x*>)) - A = ((p ^ q) ^ <*x*>) - A by FINSEQ_1:32

.= ((p ^ q) - A) ^ (<*x*> - A) by Lm9

.= ((p - A) ^ (q - A)) ^ (<*x*> - A) by A1

.= (p - A) ^ ((q - A) ^ (<*x*> - A)) by FINSEQ_1:32

.= (p - A) ^ ((q ^ <*x*>) - A) by Lm9 ; :: thesis: verum

end;
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) holds

for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

let x be set ; :: thesis: ( ( for p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) implies for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A) )

assume A1: for p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ; :: thesis: for p being FinSequence

for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

let p be FinSequence; :: thesis: for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

let A be set ; :: thesis: (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)

thus (p ^ (q ^ <*x*>)) - A = ((p ^ q) ^ <*x*>) - A by FINSEQ_1:32

.= ((p ^ q) - A) ^ (<*x*> - A) by Lm9

.= ((p - A) ^ (q - A)) ^ (<*x*> - A) by A1

.= (p - A) ^ ((q - A) ^ (<*x*> - A)) by FINSEQ_1:32

.= (p - A) ^ ((q ^ <*x*>) - A) by Lm9 ; :: thesis: verum

Lm11: for q, p being FinSequence

for A being set holds (p ^ q) - A = (p - A) ^ (q - A)

proof end;

theorem :: FINSEQ_3:73

theorem Th83: :: FINSEQ_3:83

for p, q being FinSequence

for A being set

for k being Nat st len p = k + 1 & q = p | (Seg k) holds

( p . (k + 1) in A iff p - A = q - A )

for A being set

for k being Nat st len p = k + 1 & q = p | (Seg k) holds

( p . (k + 1) in A iff p - A = q - A )

proof end;

theorem Th84: :: FINSEQ_3:84

for p, q being FinSequence

for A being set

for k being Nat st len p = k + 1 & q = p | (Seg k) holds

( not p . (k + 1) in A iff p - A = (q - A) ^ <*(p . (k + 1))*> )

for A being set

for k being Nat st len p = k + 1 & q = p | (Seg k) holds

( not p . (k + 1) in A iff p - A = (q - A) ^ <*(p . (k + 1))*> )

proof end;

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 )

proof end;

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 )

proof end;

theorem :: FINSEQ_3:85

for p being FinSequence

for A being set

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 )

for A being set

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 )

proof end;

theorem Th88: :: FINSEQ_3:88

for p being FinSequence

for A being set st p is one-to-one holds

len (p - A) = (len p) - (card (A /\ (rng p)))

for A being set st p is one-to-one holds

len (p - A) = (len p) - (card (A /\ (rng p)))

proof end;

theorem Th89: :: FINSEQ_3:89

for p being FinSequence

for A being finite set st p is one-to-one & A c= rng p holds

len (p - A) = (len p) - (card A)

for A being finite set st p is one-to-one & A c= rng p holds

len (p - A) = (len p) - (card A)

proof end;

theorem :: FINSEQ_3:90

for p being FinSequence

for x being set st p is one-to-one & x in rng p holds

len (p - {x}) = (len p) - 1

for x being set st p is one-to-one & x in rng p holds

len (p - {x}) = (len p) - 1

proof end;

theorem Th91: :: FINSEQ_3:91

for p, q being FinSequence holds

( ( rng p misses rng q & p is one-to-one & q is one-to-one ) iff p ^ q is one-to-one )

( ( rng p misses rng q & p is one-to-one & q is one-to-one ) iff p ^ q is one-to-one )

proof end;

theorem :: FINSEQ_3:92

theorem Th98: :: FINSEQ_3:98

for p being FinSequence

for x, y being set st p is one-to-one & rng p = {x,y} & x <> y holds

len p = 2

for x, y being set st p is one-to-one & rng p = {x,y} & x <> y holds

len p = 2

proof end;

theorem :: FINSEQ_3:99

for p being FinSequence

for x, y being set st p is one-to-one & rng p = {x,y} & x <> y & not p = <*x,y*> holds

p = <*y,x*>

for x, y being set st p is one-to-one & rng p = {x,y} & x <> y & not p = <*x,y*> holds

p = <*y,x*>

proof end;

theorem Th100: :: FINSEQ_3:100

for p being FinSequence

for x, y, z being set st p is one-to-one & rng p = {x,y,z} & <*x,y,z*> is one-to-one holds

len p = 3

for x, y, z being set st p is one-to-one & rng p = {x,y,z} & <*x,y,z*> is one-to-one holds

len p = 3

proof end;

theorem :: FINSEQ_3:101

for p being FinSequence

for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z holds

len p = 3

for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z holds

len p = 3

proof end;

begin

:: from FSM_1

theorem :: FINSEQ_3:102

for D being non empty set

for df being FinSequence of D st not df is empty holds

ex d being Element of D ex df1 being FinSequence of D st

( d = df . 1 & df = <*d*> ^ df1 )

for df being FinSequence of D st not df is empty holds

ex d being Element of D ex df1 being FinSequence of D st

( d = df . 1 & df = <*d*> ^ df1 )

proof end;

theorem :: FINSEQ_3:103

for i being Nat

for df being FinSequence

for d being set st i in dom df holds

(<*d*> ^ df) . (i + 1) = df . i

for df being FinSequence

for d being set st i in dom df holds

(<*d*> ^ df) . (i + 1) = df . i

proof end;

:: from MATRIX_2, 2005.11.16, A.T.

definition
end;

:: deftheorem defines Del FINSEQ_3:def 2 :

for i being Nat

for p being FinSequence holds Del (p,i) = p * (Sgm ((dom p) \ {i}));

for i being Nat

for p being FinSequence holds Del (p,i) = p * (Sgm ((dom p) \ {i}));

theorem Th104: :: FINSEQ_3:104

for i being Nat

for p being FinSequence holds

( ( i in dom p implies ex m being Nat st

( len p = m + 1 & len (Del (p,i)) = m ) ) & ( not i in dom p implies Del (p,i) = p ) )

for p being FinSequence holds

( ( i in dom p implies ex m being Nat st

( len p = m + 1 & len (Del (p,i)) = m ) ) & ( not i in dom p implies Del (p,i) = p ) )

proof end;

theorem :: FINSEQ_3:105

for i being Nat

for D being non empty set

for p being FinSequence of D holds Del (p,i) is FinSequence of D

for D being non empty set

for p being FinSequence of D holds Del (p,i) is FinSequence of D

proof end;

:: from MATRLIN, 2005.11.16, A.T.

:: from GOBOARD1, 2005.11.16, A.T.

theorem Th108: :: FINSEQ_3:108

for i, k, m, n being Nat st n = m + 1 & k in Seg n & i in Seg m holds

( ( 1 <= i & i < k implies (Sgm ((Seg n) \ {k})) . i = i ) & ( k <= i & i <= m implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) )

( ( 1 <= i & i < k implies (Sgm ((Seg n) \ {k})) . i = i ) & ( k <= i & i <= m implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) )

proof end;

theorem :: FINSEQ_3:111

for m, n, k being Nat

for f being FinSequence st len f = m + 1 & n in dom f & n <= k & k <= m holds

(Del (f,n)) . k = f . (k + 1)

for f being FinSequence st len f = m + 1 & n in dom f & n <= k & k <= m holds

(Del (f,n)) . k = f . (k + 1)

proof end;

:: from JORDAN3, 2005.11.16, A.T.

:: missing, 27.11.2005, A.T.

:: from MATRLIN, 2006.01.06, A.T.

theorem Th114: :: FINSEQ_3:114

for A being set

for F being FinSequence holds (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F)

for F being FinSequence holds (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F)

proof end;

theorem :: FINSEQ_3:115

for F being FinSequence

for A being Subset of (rng F) ex p being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * p

for A being Subset of (rng F) ex p being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * p

proof end;

:: Moved from GRAPH_2 by AK on 27.12.2006

:: Moved from SCMBSORT by AK on 10.10.2007

:: missing, 2008.02.16, A.T,

:: from CATALG_1, 2009.09.08, A.T.

:: from AMISTD_2, 2009.09.08, A.T.

registration
end;

begin

theorem :: FINSEQ_3:120

for D1, D2 being non empty set

for p being FinSequence of D1

for f being Function of D1,D2 holds

( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds

(f * p) . n = f . (p . n) ) )

for p being FinSequence of D1

for f being Function of D1,D2 holds

( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds

(f * p) . n = f . (p . n) ) )

proof end;

definition

let D be non empty set ;

let R be Relation of D;

ex b_{1} being Relation of (D *) st

for x, y being FinSequence of D holds

( [x,y] in b_{1} iff ( len x = len y & ( for n being Element of NAT st n in dom x holds

[(x . n),(y . n)] in R ) ) )

for b_{1}, b_{2} being Relation of (D *) st ( for x, y being FinSequence of D holds

( [x,y] in b_{1} 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 b_{2} iff ( len x = len y & ( for n being Element of NAT st n in dom x holds

[(x . n),(y . n)] in R ) ) ) ) holds

b_{1} = b_{2}

end;
let R be Relation of D;

func ExtendRel R -> Relation of (D *) means :Def3: :: FINSEQ_3:def 3

for x, y being FinSequence of D holds

( [x,y] in it iff ( len x = len y & ( for n being Element of NAT st n in dom x holds

[(x . n),(y . n)] in R ) ) );

existence for x, y being FinSequence of D holds

( [x,y] in it iff ( len x = len y & ( for n being Element of NAT st n in dom x holds

[(x . n),(y . n)] in R ) ) );

ex b

for x, y being FinSequence of D holds

( [x,y] in b

[(x . n),(y . n)] in R ) ) )

proof end;

uniqueness for b

( [x,y] in b

[(x . n),(y . n)] in R ) ) ) ) & ( for x, y being FinSequence of D holds

( [x,y] in b

[(x . n),(y . n)] in R ) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines ExtendRel FINSEQ_3:def 3 :

for D being non empty set

for R being Relation of D

for b_{3} being Relation of (D *) holds

( b_{3} = ExtendRel R iff for x, y being FinSequence of D holds

( [x,y] in b_{3} iff ( len x = len y & ( for n being Element of NAT st n in dom x holds

[(x . n),(y . n)] in R ) ) ) );

for D being non empty set

for R being Relation of D

for b

( b

( [x,y] in b

[(x . n),(y . n)] in R ) ) ) );

definition

let D be non empty set ;

let R be Equivalence_Relation of D;

let y be FinSequence of Class R;

let x be FinSequence of D;

end;
let R be Equivalence_Relation of D;

let y be FinSequence of Class R;

let x be FinSequence of D;

:: deftheorem defines is_representatives_FS FINSEQ_3:def 4 :

for D being non empty set

for R being Equivalence_Relation of D

for y being FinSequence of Class R

for x being FinSequence of D holds

( x is_representatives_FS y iff ( len x = len y & ( for n being Element of NAT st n in dom x holds

Class (R,(x . n)) = y . n ) ) );

for D being non empty set

for R being Equivalence_Relation of D

for y being FinSequence of Class R

for x being FinSequence of D holds

( x is_representatives_FS y iff ( len x = len y & ( for n being Element of NAT st n in dom x holds

Class (R,(x . n)) = y . n ) ) );

theorem :: FINSEQ_3:122

for D being non empty set

for R being Equivalence_Relation of D

for y being FinSequence of Class R ex x being FinSequence of D st x is_representatives_FS y

for R being Equivalence_Relation of D

for y being FinSequence of Class R ex x being FinSequence of D st x is_representatives_FS y

proof end;

theorem Th124: :: FINSEQ_3:124

for z, X, Y being set holds

( z in product <*X,Y*> iff ex x, y being set st

( x in X & y in Y & z = <*x,y*> ) )

( z in product <*X,Y*> iff ex x, y being set st

( x in X & y in Y & z = <*x,y*> ) )

proof end;

theorem Th125: :: FINSEQ_3:125

for a, X, Y, Z being set holds

( a in product <*X,Y,Z*> iff ex x, y, z being set st

( x in X & y in Y & z in Z & a = <*x,y,z*> ) )

( a in product <*X,Y,Z*> iff ex x, y, z being set st

( x in X & y in Y & z in Z & a = <*x,y,z*> ) )

proof end;

theorem Th127: :: FINSEQ_3:127

for D1, D2 being non empty set holds product <*D1,D2*> = { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum }

proof end;

theorem Th129: :: FINSEQ_3:129

for D1, D2, D3 being non empty set holds product <*D1,D2,D3*> = { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum }

proof end;

theorem Th133: :: FINSEQ_3:133

for f, g being Function holds

( doms <*f,g*> = <*(dom f),(dom g)*> & rngs <*f,g*> = <*(rng f),(rng g)*> )

( doms <*f,g*> = <*(dom f),(dom g)*> & rngs <*f,g*> = <*(rng f),(rng g)*> )

proof end;

theorem :: FINSEQ_3:134

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)*> )

( doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> & rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> )

proof end;

theorem :: FINSEQ_3:138

for x being set

for f, g, h being Function st x in dom f holds

( <*f*> .. (1,x) = f . x & <*f,g*> .. (1,x) = f . x & <*f,g,h*> .. (1,x) = f . x )

for f, g, h being Function st x in dom f holds

( <*f*> .. (1,x) = f . x & <*f,g*> .. (1,x) = f . x & <*f,g,h*> .. (1,x) = f . x )

proof end;

theorem :: FINSEQ_3:139

for x being set

for g, f, h being Function st x in dom g holds

( <*f,g*> .. (2,x) = g . x & <*f,g,h*> .. (2,x) = g . x )

for g, f, h being Function st x in dom g holds

( <*f,g*> .. (2,x) = g . x & <*f,g,h*> .. (2,x) = g . x )

proof end;

theorem :: FINSEQ_3:141

for h being Function holds

( dom <:<*h*>:> = dom h & ( for x being set st x in dom h holds

<:<*h*>:> . x = <*(h . x)*> ) )

( dom <:<*h*>:> = dom h & ( for x being set st x in dom h holds

<:<*h*>:> . x = <*(h . x)*> ) )

proof end;

theorem Th142: :: FINSEQ_3:142

for f1, f2 being Function holds

( dom <:<*f1,f2*>:> = (dom f1) /\ (dom f2) & ( for x being set st x in (dom f1) /\ (dom f2) holds

<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> ) )

( dom <:<*f1,f2*>:> = (dom f1) /\ (dom f2) & ( for x being set st x in (dom f1) /\ (dom f2) holds

<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> ) )

proof end;

theorem :: FINSEQ_3:143

for h being Function holds

( dom (Frege <*h*>) = product <*(dom h)*> & rng (Frege <*h*>) = product <*(rng h)*> & ( for x being set st x in dom h holds

(Frege <*h*>) . <*x*> = <*(h . x)*> ) )

( dom (Frege <*h*>) = product <*(dom h)*> & rng (Frege <*h*>) = product <*(rng h)*> & ( for x being set st x in dom h holds

(Frege <*h*>) . <*x*> = <*(h . x)*> ) )

proof end;

theorem Th144: :: FINSEQ_3:144

for f1, f2 being Function holds

( dom (Frege <*f1,f2*>) = product <*(dom f1),(dom f2)*> & rng (Frege <*f1,f2*>) = product <*(rng f1),(rng f2)*> & ( for x, y being set st x in dom f1 & y in dom f2 holds

(Frege <*f1,f2*>) . <*x,y*> = <*(f1 . x),(f2 . y)*> ) )

( dom (Frege <*f1,f2*>) = product <*(dom f1),(dom f2)*> & rng (Frege <*f1,f2*>) = product <*(rng f1),(rng f2)*> & ( for x, y being set st x in dom f1 & y in dom f2 holds

(Frege <*f1,f2*>) . <*x,y*> = <*(f1 . x),(f2 . y)*> ) )

proof end;

theorem :: FINSEQ_3:145

for x being set

for f1, f2 being Function st x in dom f1 & x in dom f2 holds

for y1, y2 being set holds

( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> )

for f1, f2 being Function st x in dom f1 & x in dom f2 holds

for y1, y2 being set holds

( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> )

proof end;

theorem :: FINSEQ_3:146

for x, y being set

for f1, f2 being Function st x in dom f1 & y in dom f2 holds

for y1, y2 being set holds

( [:f1,f2:] . (x,y) = [y1,y2] iff (Frege <*f1,f2*>) . <*x,y*> = <*y1,y2*> )

for f1, f2 being Function st x in dom f1 & y in dom f2 holds

for y1, y2 being set holds

( [:f1,f2:] . (x,y) = [y1,y2] iff (Frege <*f1,f2*>) . <*x,y*> = <*y1,y2*> )

proof end;

::from JORDAN2C, 2011.07.03, A.T.

theorem :: FINSEQ_3:151

for x, y being set

for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds

( f . 1 = y & f . 2 = x )

for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds

( f . 1 = y & f . 2 = x )

proof end;

:: from GLIB_001, 2011.07.30, A.T.

theorem :: FINSEQ_3:152

for X being set

for k being Element of NAT st X c= Seg k holds

for m, n being Element of NAT st m in dom (Sgm X) & n = (Sgm X) . m holds

m <= n

for k being Element of NAT st X c= Seg k holds

for m, n being Element of NAT st m in dom (Sgm X) & n = (Sgm X) . m holds

m <= n

proof end;

:: proved in RLVECT_1 and has a number 104.