:: FINSEQ_1 semantic presentation
begin
definition
let n be Nat;
func Seg n -> set equals :: FINSEQ_1:def 1
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } ;
correctness
coherence
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } is set ;
;
end;
:: deftheorem defines Seg FINSEQ_1:def_1_:_
for n being Nat holds Seg n = { k where k is Element of NAT : ( 1 <= k & k <= n ) } ;
definition
let n be Nat;
:: original: Seg
redefine func Seg n -> Subset of NAT;
coherence
Seg n is Subset of NAT
proof
set X = Seg n;
Seg n c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg n or x in NAT )
assume x in Seg n ; ::_thesis: x in NAT
then ex k being Element of NAT st
( x = k & 1 <= k & k <= n ) ;
hence x in NAT ; ::_thesis: verum
end;
hence Seg n is Subset of NAT ; ::_thesis: verum
end;
end;
theorem Th1: :: FINSEQ_1:1
for a, b being Nat holds
( a in Seg b iff ( 1 <= a & a <= b ) )
proof
let a, b be Nat; ::_thesis: ( a in Seg b iff ( 1 <= a & a <= b ) )
A1: a in NAT by ORDINAL1:def_12;
( a in { m where m is Element of NAT : ( 1 <= m & m <= b ) } iff ex m being Element of NAT st
( a = m & 1 <= m & m <= b ) ) ;
hence ( a in Seg b iff ( 1 <= a & a <= b ) ) by A1; ::_thesis: verum
end;
registration
let n be zero Nat;
cluster Seg n -> empty ;
coherence
Seg n is empty
proof
assume not Seg n is empty ; ::_thesis: contradiction
then consider x being set such that
A1: x in Seg n by XBOOLE_0:def_1;
ex k being Element of NAT st
( k = x & 1 <= k & k <= 0 ) by A1;
hence contradiction ; ::_thesis: verum
end;
end;
theorem Th2: :: FINSEQ_1:2
( Seg 1 = {1} & Seg 2 = {1,2} )
proof
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Seg_1_implies_x_in_{1}_)_&_(_x_in_{1}_implies_x_in_Seg_1_)_)
let x be set ; ::_thesis: ( ( x in Seg 1 implies x in {1} ) & ( x in {1} implies x in Seg 1 ) )
thus ( x in Seg 1 implies x in {1} ) ::_thesis: ( x in {1} implies x in Seg 1 )
proof
assume x in Seg 1 ; ::_thesis: x in {1}
then consider k being Element of NAT such that
A1: x = k and
A2: ( 1 <= k & k <= 1 ) ;
k = 1 by A2, XXREAL_0:1;
hence x in {1} by A1, TARSKI:def_1; ::_thesis: verum
end;
assume x in {1} ; ::_thesis: x in Seg 1
then x = 1 by TARSKI:def_1;
hence x in Seg 1 ; ::_thesis: verum
end;
hence Seg 1 = {1} by TARSKI:1; ::_thesis: Seg 2 = {1,2}
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Seg_2_implies_x_in_{1,2}_)_&_(_x_in_{1,2}_implies_x_in_Seg_2_)_)
let x be set ; ::_thesis: ( ( x in Seg 2 implies x in {1,2} ) & ( x in {1,2} implies x in Seg 2 ) )
thus ( x in Seg 2 implies x in {1,2} ) ::_thesis: ( x in {1,2} implies x in Seg 2 )
proof
assume x in Seg 2 ; ::_thesis: x in {1,2}
then consider k being Element of NAT such that
A3: x = k and
A4: 1 <= k and
A5: k <= 2 ;
k <= 1 + 1 by A5;
then ( k = 1 or k = 2 ) by A4, NAT_1:9;
hence x in {1,2} by A3, TARSKI:def_2; ::_thesis: verum
end;
assume x in {1,2} ; ::_thesis: x in Seg 2
then ( x = 1 or x = 2 ) by TARSKI:def_2;
hence x in Seg 2 ; ::_thesis: verum
end;
hence Seg 2 = {1,2} by TARSKI:1; ::_thesis: verum
end;
theorem Th3: :: FINSEQ_1:3
for a being Nat holds
( a = 0 or a in Seg a )
proof
let a be Nat; ::_thesis: ( a = 0 or a in Seg a )
assume a <> 0 ; ::_thesis: a in Seg a
then ex b being Nat st a = b + 1 by NAT_1:6;
then ( a in NAT & 1 <= a ) by NAT_1:11;
hence a in Seg a ; ::_thesis: verum
end;
registration
let n be non zero Nat;
cluster Seg n -> non empty ;
coherence
not Seg n is empty by Th3;
end;
theorem :: FINSEQ_1:4
for a being Nat holds a + 1 in Seg (a + 1) by Th3;
theorem Th5: :: FINSEQ_1:5
for a, b being Nat holds
( a <= b iff Seg a c= Seg b )
proof
let a, b be Nat; ::_thesis: ( a <= b iff Seg a c= Seg b )
thus ( a <= b implies Seg a c= Seg b ) ::_thesis: ( Seg a c= Seg b implies a <= b )
proof
assume A1: a <= b ; ::_thesis: Seg a c= Seg b
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg a or x in Seg b )
assume A2: x in Seg a ; ::_thesis: x in Seg b
then reconsider c = x as Element of NAT ;
A3: 1 <= c by A2, Th1;
c <= a by A2, Th1;
then c <= b by A1, XXREAL_0:2;
hence x in Seg b by A3; ::_thesis: verum
end;
assume A4: Seg a c= Seg b ; ::_thesis: a <= b
now__::_thesis:_(_a_<>_0_implies_a_<=_b_)
assume a <> 0 ; ::_thesis: a <= b
then a in Seg a by Th3;
hence a <= b by A4, Th1; ::_thesis: verum
end;
hence a <= b ; ::_thesis: verum
end;
theorem Th6: :: FINSEQ_1:6
for a, b being Nat st Seg a = Seg b holds
a = b
proof
let a, b be Nat; ::_thesis: ( Seg a = Seg b implies a = b )
assume Seg a = Seg b ; ::_thesis: a = b
then ( a <= b & b <= a ) by Th5;
hence a = b by XXREAL_0:1; ::_thesis: verum
end;
theorem Th7: :: FINSEQ_1:7
for c, a being Nat st c <= a holds
Seg c = (Seg a) /\ (Seg c)
proof
let c, a be Nat; ::_thesis: ( c <= a implies Seg c = (Seg a) /\ (Seg c) )
assume c <= a ; ::_thesis: Seg c = (Seg a) /\ (Seg c)
then Seg c c= Seg a by Th5;
hence Seg c = (Seg a) /\ (Seg c) by XBOOLE_1:28; ::_thesis: verum
end;
theorem :: FINSEQ_1:8
for c, a being Nat st Seg c = (Seg c) /\ (Seg a) holds
c <= a by Th6, Th7;
theorem Th9: :: FINSEQ_1:9
for a being Nat holds (Seg a) \/ {(a + 1)} = Seg (a + 1)
proof
let a be Nat; ::_thesis: (Seg a) \/ {(a + 1)} = Seg (a + 1)
thus (Seg a) \/ {(a + 1)} c= Seg (a + 1) :: according to XBOOLE_0:def_10 ::_thesis: Seg (a + 1) c= (Seg a) \/ {(a + 1)}
proof
a + 0 <= a + 1 by XREAL_1:7;
then A1: Seg a c= Seg (a + 1) by Th5;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Seg a) \/ {(a + 1)} or x in Seg (a + 1) )
assume x in (Seg a) \/ {(a + 1)} ; ::_thesis: x in Seg (a + 1)
then ( x in Seg a or x in {(a + 1)} ) by XBOOLE_0:def_3;
then ( x in Seg (a + 1) or x = a + 1 ) by A1, TARSKI:def_1;
hence x in Seg (a + 1) by Th3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (a + 1) or x in (Seg a) \/ {(a + 1)} )
assume A2: x in Seg (a + 1) ; ::_thesis: x in (Seg a) \/ {(a + 1)}
then reconsider x = x as Element of NAT ;
A3: x <= a + 1 by A2, Th1;
A4: 1 <= x by A2, Th1;
( x <= a or x = a + 1 ) by A3, NAT_1:8;
then ( x in Seg a or x in {(a + 1)} ) by A4, TARSKI:def_1;
hence x in (Seg a) \/ {(a + 1)} by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: FINSEQ_1:10
for k being Nat holds Seg k = (Seg (k + 1)) \ {(k + 1)}
proof
let k be Nat; ::_thesis: Seg k = (Seg (k + 1)) \ {(k + 1)}
A1: Seg (k + 1) = (Seg k) \/ {(k + 1)} by Th9;
Seg k misses {(k + 1)}
proof
assume not Seg k misses {(k + 1)} ; ::_thesis: contradiction
then A2: (Seg k) /\ {(k + 1)} <> {} by XBOOLE_0:def_7;
set x = the Element of (Seg k) /\ {(k + 1)};
A3: the Element of (Seg k) /\ {(k + 1)} in Seg k by A2, XBOOLE_0:def_4;
then reconsider x = the Element of (Seg k) /\ {(k + 1)} as Element of NAT ;
x in {(k + 1)} by A2, XBOOLE_0:def_4;
then A4: x = k + 1 by TARSKI:def_1;
x <= k by A3, Th1;
hence contradiction by A4, XREAL_1:29; ::_thesis: verum
end;
hence Seg k = (Seg (k + 1)) \ {(k + 1)} by A1, XBOOLE_1:88; ::_thesis: verum
end;
definition
let IT be Relation;
attrIT is FinSequence-like means :Def2: :: FINSEQ_1:def 2
ex n being Nat st dom IT = Seg n;
end;
:: deftheorem Def2 defines FinSequence-like FINSEQ_1:def_2_:_
for IT being Relation holds
( IT is FinSequence-like iff ex n being Nat st dom IT = Seg n );
registration
cluster Relation-like empty -> FinSequence-like for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is FinSequence-like
proof
let R be Relation; ::_thesis: ( R is empty implies R is FinSequence-like )
assume A1: R is empty ; ::_thesis: R is FinSequence-like
take 0 ; :: according to FINSEQ_1:def_2 ::_thesis: dom R = Seg 0
thus dom R = Seg 0 by A1; ::_thesis: verum
end;
end;
definition
mode FinSequence is FinSequence-like Function;
end;
defpred S1[ set , set ] means ex k being Nat st
( $1 = k & $2 = k + 1 );
registration
let n be Nat;
cluster Seg n -> finite ;
coherence
Seg n is finite
proof
Seg n is finite
proof
A1: n = { k where k is Element of NAT : k < n } by AXIOMS:4;
A2: for x being set st x in n holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in n implies ex y being set st S1[x,y] )
assume x in n ; ::_thesis: ex y being set st S1[x,y]
then ex k being Element of NAT st
( x = k & k < n ) by A1;
then reconsider k = x as Nat ;
take k + 1 ; ::_thesis: S1[x,k + 1]
thus S1[x,k + 1] ; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = n and
A4: for x being set st x in n holds
S1[x,f . x] from CLASSES1:sch_1(A2);
take f ; :: according to FINSET_1:def_1 ::_thesis: ( rng f = Seg n & dom f in omega )
thus rng f = Seg n ::_thesis: dom f in omega
proof
thus rng f c= Seg n :: according to XBOOLE_0:def_10 ::_thesis: Seg n c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Seg n )
assume x in rng f ; ::_thesis: x in Seg n
then consider y being set such that
A5: y in dom f and
A6: x = f . y by FUNCT_1:def_3;
consider k being Nat such that
A7: y = k and
A8: x = k + 1 by A3, A4, A5, A6;
ex m being Element of NAT st
( m = y & m < n ) by A1, A3, A5;
then ( 1 <= k + 1 & k + 1 <= n ) by A7, NAT_1:11, NAT_1:13;
hence x in Seg n by A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg n or x in rng f )
assume x in Seg n ; ::_thesis: x in rng f
then consider k being Element of NAT such that
A9: x = k and
A10: 1 <= k and
A11: k <= n ;
consider i being Nat such that
A12: 1 + i = k by A10, NAT_1:10;
( i in NAT & i < n ) by A11, A12, NAT_1:13, ORDINAL1:def_12;
then A13: i in n by A1;
then S1[i,f . i] by A4;
hence x in rng f by A3, A9, A12, A13, FUNCT_1:def_3; ::_thesis: verum
end;
thus dom f in omega by A3, ORDINAL1:def_12; ::_thesis: verum
end;
hence Seg n is finite ; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like FinSequence-like -> finite for set ;
coherence
for b1 being Function st b1 is FinSequence-like holds
b1 is finite
proof
let f be Function; ::_thesis: ( f is FinSequence-like implies f is finite )
given n being Nat such that A1: dom f = Seg n ; :: according to FINSEQ_1:def_2 ::_thesis: f is finite
rng f is finite by A1, FINSET_1:8;
then [:(dom f),(rng f):] is finite by A1;
hence f is finite by FINSET_1:1, RELAT_1:7; ::_thesis: verum
end;
end;
Lm1: for n being Nat holds Seg n,n are_equipotent
proof
let n be Nat; ::_thesis: Seg n,n are_equipotent
defpred S2[ Nat] means Seg $1,$1 are_equipotent ;
A1: S2[ 0 ] ;
A2: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A3: Seg n,n are_equipotent ; ::_thesis: S2[n + 1]
A4: n + 1 = succ n by NAT_1:38
.= n \/ {n} by ORDINAL1:def_1 ;
A5: ( Seg (n + 1) = (Seg n) \/ {(n + 1)} & {(n + 1)},{n} are_equipotent ) by Th9, CARD_1:28;
A6: now__::_thesis:_not_n_meets_{n}
assume n meets {n} ; ::_thesis: contradiction
then consider x being set such that
A7: x in n and
A8: x in {n} by XBOOLE_0:3;
x = n by A8, TARSKI:def_1;
hence contradiction by A7; ::_thesis: verum
end;
now__::_thesis:_not_Seg_n_meets_{(n_+_1)}
assume Seg n meets {(n + 1)} ; ::_thesis: contradiction
then consider x being set such that
A9: x in Seg n and
A10: x in {(n + 1)} by XBOOLE_0:3;
A11: x = n + 1 by A10, TARSKI:def_1;
not n + 1 <= n by NAT_1:13;
hence contradiction by A9, A11, Th1; ::_thesis: verum
end;
hence S2[n + 1] by A3, A4, A5, A6, CARD_1:31; ::_thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch_2(A1, A2);
hence Seg n,n are_equipotent ; ::_thesis: verum
end;
Lm2: for n being Nat holds card (Seg n) = card n
proof
let n be Nat; ::_thesis: card (Seg n) = card n
Seg n,n are_equipotent by Lm1;
hence card (Seg n) = card n by CARD_1:5; ::_thesis: verum
end;
registration
let n be Nat;
cluster Seg n -> n -element ;
coherence
Seg n is n -element
proof
card (Seg n) = card n by Lm2;
hence card (Seg n) = n by CARD_1:def_2; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
notation
let p be FinSequence;
synonym len p for card p;
end;
definition
let p be FinSequence;
:: original: len
redefine func len p -> Element of NAT means :Def3: :: FINSEQ_1:def 3
Seg it = dom p;
coherence
len p is Element of NAT
proof
card p = card p ;
hence len p is Element of NAT ; ::_thesis: verum
end;
compatibility
for b1 being Element of NAT holds
( b1 = len p iff Seg b1 = dom p )
proof
let k be Element of NAT ; ::_thesis: ( k = len p iff Seg k = dom p )
consider n being Nat such that
A1: dom p = Seg n by Def2;
dom p,p are_equipotent
proof
deffunc H1( set ) -> set = [$1,(p . $1)];
consider g being Function such that
A2: dom g = dom p and
A3: for x being set st x in dom p holds
g . x = H1(x) from FUNCT_1:sch_3();
take g ; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & dom g = dom p & rng g = p )
thus g is one-to-one ::_thesis: ( dom g = dom p & rng g = p )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom g or not b1 in dom g or not g . x = g . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume that
A4: x in dom g and
A5: y in dom g ; ::_thesis: ( not g . x = g . y or x = y )
assume g . x = g . y ; ::_thesis: x = y
then [x,(p . x)] = g . y by A2, A3, A4
.= [y,(p . y)] by A2, A3, A5 ;
hence x = y by XTUPLE_0:1; ::_thesis: verum
end;
thus dom g = dom p by A2; ::_thesis: rng g = p
thus rng g c= p :: according to XBOOLE_0:def_10 ::_thesis: p c= rng g
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng g or i in p )
assume i in rng g ; ::_thesis: i in p
then consider x being set such that
A6: x in dom g and
A7: g . x = i by FUNCT_1:def_3;
g . x = [x,(p . x)] by A2, A3, A6;
hence i in p by A2, A6, A7, FUNCT_1:1; ::_thesis: verum
end;
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in p or [x,y] in rng g )
assume A8: [x,y] in p ; ::_thesis: [x,y] in rng g
then A9: x in dom p by FUNCT_1:1;
y = p . x by A8, FUNCT_1:1;
then g . x = [x,y] by A3, A9;
hence [x,y] in rng g by A2, A9, FUNCT_1:def_3; ::_thesis: verum
end;
then A10: card p = card (dom p) by CARD_1:5;
thus ( k = card p implies Seg k = dom p ) ::_thesis: ( Seg k = dom p implies k = len p )
proof
assume k = card p ; ::_thesis: Seg k = dom p
then k = card n by A1, A10, Lm2;
hence Seg k = dom p by A1, CARD_1:def_2; ::_thesis: verum
end;
assume A11: Seg k = dom p ; ::_thesis: k = len p
thus k = card k by CARD_1:def_2
.= card p by A10, A11, Lm2 ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines len FINSEQ_1:def_3_:_
for p being FinSequence
for b2 being Element of NAT holds
( b2 = len p iff Seg b2 = dom p );
definition
let p be FinSequence;
:: original: dom
redefine func dom p -> Subset of NAT;
coherence
dom p is Subset of NAT
proof
dom p = Seg (len p) by Def3;
hence dom p is Subset of NAT ; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:11
for f being Function st ex k being Nat st dom f c= Seg k holds
ex p being FinSequence st f c= p
proof
let f be Function; ::_thesis: ( ex k being Nat st dom f c= Seg k implies ex p being FinSequence st f c= p )
given k being Nat such that A1: dom f c= Seg k ; ::_thesis: ex p being FinSequence st f c= p
deffunc H1( set ) -> set = f . $1;
consider g being Function such that
A2: ( dom g = Seg k & ( for x being set st x in Seg k holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider g = g as FinSequence by A2, Def2;
take g ; ::_thesis: f c= g
let y, z be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [y,z] in f or [y,z] in g )
assume A3: [y,z] in f ; ::_thesis: [y,z] in g
then A4: y in dom f by XTUPLE_0:def_12;
then A5: f . y = z by A3, FUNCT_1:def_2;
[y,(g . y)] in g by A1, A2, A4, FUNCT_1:1;
hence [y,z] in g by A1, A2, A4, A5; ::_thesis: verum
end;
scheme :: FINSEQ_1:sch 1
SeqEx{ F1() -> Nat, P1[ set , set ] } :
ex p being FinSequence st
( dom p = Seg F1() & ( for k being Nat st k in Seg F1() holds
P1[k,p . k] ) )
provided
A1: for k being Nat st k in Seg F1() holds
ex x being set st P1[k,x]
proof
A2: for x being set st x in Seg F1() holds
ex y being set st P1[x,y] by A1;
consider f being Function such that
A3: ( dom f = Seg F1() & ( for x being set st x in Seg F1() holds
P1[x,f . x] ) ) from CLASSES1:sch_1(A2);
reconsider p = f as FinSequence by A3, Def2;
take p ; ::_thesis: ( dom p = Seg F1() & ( for k being Nat st k in Seg F1() holds
P1[k,p . k] ) )
thus ( dom p = Seg F1() & ( for k being Nat st k in Seg F1() holds
P1[k,p . k] ) ) by A3; ::_thesis: verum
end;
scheme :: FINSEQ_1:sch 2
SeqLambda{ F1() -> Nat, F2( set ) -> set } :
ex p being FinSequence st
( len p = F1() & ( for k being Nat st k in dom p holds
p . k = F2(k) ) )
proof
consider f being Function such that
A1: ( dom f = Seg F1() & ( for x being set st x in Seg F1() holds
f . x = F2(x) ) ) from FUNCT_1:sch_3();
A2: F1() in NAT by ORDINAL1:def_12;
reconsider p = f as FinSequence by A1, Def2;
take p ; ::_thesis: ( len p = F1() & ( for k being Nat st k in dom p holds
p . k = F2(k) ) )
thus ( len p = F1() & ( for k being Nat st k in dom p holds
p . k = F2(k) ) ) by A1, A2, Def3; ::_thesis: verum
end;
theorem :: FINSEQ_1:12
for z being set
for p being FinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )
proof
let z be set ; ::_thesis: for p being FinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )
let p be FinSequence; ::_thesis: ( z in p implies ex k being Nat st
( k in dom p & z = [k,(p . k)] ) )
assume A1: z in p ; ::_thesis: ex k being Nat st
( k in dom p & z = [k,(p . k)] )
then consider x, y being set such that
A2: z = [x,y] by RELAT_1:def_1;
x in dom p by A1, A2, FUNCT_1:1;
then reconsider k = x as Nat ;
take k ; ::_thesis: ( k in dom p & z = [k,(p . k)] )
thus ( k in dom p & z = [k,(p . k)] ) by A1, A2, FUNCT_1:1; ::_thesis: verum
end;
theorem Th13: :: FINSEQ_1:13
for p, q being FinSequence st dom p = dom q & ( for k being Nat st k in dom p holds
p . k = q . k ) holds
p = q
proof
let p, q be FinSequence; ::_thesis: ( dom p = dom q & ( for k being Nat st k in dom p holds
p . k = q . k ) implies p = q )
assume that
A1: dom p = dom q and
A2: for k being Nat st k in dom p holds
p . k = q . k ; ::_thesis: p = q
for x being set st x in dom p holds
p . x = q . x by A2;
hence p = q by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th14: :: FINSEQ_1:14
for p, q being FinSequence st len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) holds
p = q
proof
let p, q be FinSequence; ::_thesis: ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) implies p = q )
assume that
A1: len p = len q and
A2: for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ; ::_thesis: p = q
A3: dom p = Seg (len p) by Def3;
A4: dom q = Seg (len q) by Def3;
now__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_
p_._x_=_q_._x
let x be set ; ::_thesis: ( x in dom p implies p . x = q . x )
assume A5: x in dom p ; ::_thesis: p . x = q . x
then reconsider k = x as Nat ;
( 1 <= k & k <= len p ) by A3, A5, Th1;
hence p . x = q . x by A2; ::_thesis: verum
end;
hence p = q by A1, A3, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th15: :: FINSEQ_1:15
for a being Nat
for p being FinSequence holds p | (Seg a) is FinSequence
proof
let a be Nat; ::_thesis: for p being FinSequence holds p | (Seg a) is FinSequence
let p be FinSequence; ::_thesis: p | (Seg a) is FinSequence
A1: dom (p | (Seg a)) = (dom p) /\ (Seg a) by RELAT_1:61
.= (Seg (len p)) /\ (Seg a) by Def3 ;
( len p <= a or a <= len p ) ;
then ( dom (p | (Seg a)) = Seg (len p) or dom (p | (Seg a)) = Seg a ) by A1, Th7;
hence p | (Seg a) is FinSequence by Def2; ::_thesis: verum
end;
theorem :: FINSEQ_1:16
for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence
proof
let f be Function; ::_thesis: for p being FinSequence st rng p c= dom f holds
f * p is FinSequence
let p be FinSequence; ::_thesis: ( rng p c= dom f implies f * p is FinSequence )
assume rng p c= dom f ; ::_thesis: f * p is FinSequence
then dom (f * p) = dom p by RELAT_1:27
.= Seg (len p) by Def3 ;
hence f * p is FinSequence by Def2; ::_thesis: verum
end;
theorem Th17: :: FINSEQ_1:17
for a being Nat
for p, q being FinSequence st a <= len p & q = p | (Seg a) holds
( len q = a & dom q = Seg a )
proof
let a be Nat; ::_thesis: for p, q being FinSequence st a <= len p & q = p | (Seg a) holds
( len q = a & dom q = Seg a )
let p, q be FinSequence; ::_thesis: ( a <= len p & q = p | (Seg a) implies ( len q = a & dom q = Seg a ) )
assume that
A1: a <= len p and
A2: q = p | (Seg a) ; ::_thesis: ( len q = a & dom q = Seg a )
Seg a c= Seg (len p) by A1, Th5;
then Seg a c= dom p by Def3;
then ( a in NAT & dom q = Seg a ) by A2, ORDINAL1:def_12, RELAT_1:62;
hence ( len q = a & dom q = Seg a ) by Def3; ::_thesis: verum
end;
definition
let D be set ;
mode FinSequence of D -> FinSequence means :Def4: :: FINSEQ_1:def 4
rng it c= D;
existence
ex b1 being FinSequence st rng b1 c= D
proof
rng {} c= D by XBOOLE_1:2;
hence ex b1 being FinSequence st rng b1 c= D ; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines FinSequence FINSEQ_1:def_4_:_
for D being set
for b2 being FinSequence holds
( b2 is FinSequence of D iff rng b2 c= D );
registration
let D be set ;
cluster -> D -valued for FinSequence of D;
coherence
for b1 being FinSequence of D holds b1 is D -valued
proof
let f be FinSequence of D; ::_thesis: f is D -valued
thus rng f c= D by Def4; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
Lm3: for D being set
for f being FinSequence of D holds f is PartFunc of NAT,D
proof
let D be set ; ::_thesis: for f being FinSequence of D holds f is PartFunc of NAT,D
let f be FinSequence of D; ::_thesis: f is PartFunc of NAT,D
( dom f c= NAT & rng f c= D ) by Def4;
hence f is PartFunc of NAT,D by RELSET_1:4; ::_thesis: verum
end;
registration
cluster Relation-like empty -> FinSequence-like for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is FinSequence-like ;
end;
registration
let D be set ;
cluster Relation-like NAT -defined D -valued Function-like FinSequence-like for Element of bool [:NAT,D:];
existence
ex b1 being PartFunc of NAT,D st b1 is FinSequence-like
proof
{} is PartFunc of NAT,D by RELSET_1:12;
hence ex b1 being PartFunc of NAT,D st b1 is FinSequence-like ; ::_thesis: verum
end;
end;
definition
let D be set ;
:: original: FinSequence
redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D;
coherence
for b1 being FinSequence of D holds b1 is FinSequence-like PartFunc of NAT,D by Lm3;
end;
theorem Th18: :: FINSEQ_1:18
for a being Nat
for D being set
for p being FinSequence of D holds p | (Seg a) is FinSequence of D
proof
let a be Nat; ::_thesis: for D being set
for p being FinSequence of D holds p | (Seg a) is FinSequence of D
let D be set ; ::_thesis: for p being FinSequence of D holds p | (Seg a) is FinSequence of D
let p be FinSequence of D; ::_thesis: p | (Seg a) is FinSequence of D
A1: p | (Seg a) is FinSequence by Th15;
( rng (p | (Seg a)) c= rng p & rng p c= D ) by Def4, RELAT_1:70;
then rng (p | (Seg a)) c= D by XBOOLE_1:1;
hence p | (Seg a) is FinSequence of D by A1, Def4; ::_thesis: verum
end;
theorem :: FINSEQ_1:19
for a being Nat
for D being non empty set ex p being FinSequence of D st len p = a
proof
let a be Nat; ::_thesis: for D being non empty set ex p being FinSequence of D st len p = a
let D be non empty set ; ::_thesis: ex p being FinSequence of D st len p = a
reconsider a = a as Element of NAT by ORDINAL1:def_12;
set y = the Element of D;
set p = (Seg a) --> the Element of D;
A1: dom ((Seg a) --> the Element of D) = Seg a by FUNCOP_1:13;
then reconsider p = (Seg a) --> the Element of D as FinSequence by Def2;
( rng p c= { the Element of D} & { the Element of D} c= D ) by FUNCOP_1:13, ZFMISC_1:31;
then rng p c= D by XBOOLE_1:1;
then reconsider q = p as FinSequence of D by Def4;
take q ; ::_thesis: len q = a
thus len q = a by A1, Def3; ::_thesis: verum
end;
Lm4: for q being FinSequence holds
( q = {} iff len q = 0 )
;
theorem :: FINSEQ_1:20
for p being FinSequence holds
( p <> {} iff len p >= 1 )
proof
let p be FinSequence; ::_thesis: ( p <> {} iff len p >= 1 )
hereby ::_thesis: ( len p >= 1 implies p <> {} )
assume p <> {} ; ::_thesis: len p >= 1
then (len p) + 1 > 0 + 1 by XREAL_1:8;
hence len p >= 1 by NAT_1:13; ::_thesis: verum
end;
assume len p >= 1 ; ::_thesis: p <> {}
hence p <> {} ; ::_thesis: verum
end;
definition
let x be set ;
func<*x*> -> set equals :: FINSEQ_1:def 5
{[1,x]};
coherence
{[1,x]} is set ;
end;
:: deftheorem defines <* FINSEQ_1:def_5_:_
for x being set holds <*x*> = {[1,x]};
definition
let D be set ;
func <*> D -> FinSequence of D equals :: FINSEQ_1:def 6
{} ;
coherence
{} is FinSequence of D
proof
rng {} c= D by XBOOLE_1:2;
hence {} is FinSequence of D by Def4; ::_thesis: verum
end;
end;
:: deftheorem defines <*> FINSEQ_1:def_6_:_
for D being set holds <*> D = {} ;
registration
let D be set ;
cluster <*> D -> empty ;
coherence
<*> D is empty ;
end;
registration
let D be set ;
cluster Relation-like NAT -defined D -valued Function-like empty finite FinSequence-like for FinSequence of D;
existence
ex b1 being FinSequence of D st b1 is empty
proof
take <*> D ; ::_thesis: <*> D is empty
thus <*> D is empty ; ::_thesis: verum
end;
end;
definition
let p, q be FinSequence;
funcp ^ q -> FinSequence means :Def7: :: FINSEQ_1:def 7
( dom it = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
it . k = p . k ) & ( for k being Nat st k in dom q holds
it . ((len p) + k) = q . k ) );
existence
ex b1 being FinSequence st
( dom b1 = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b1 . k = p . k ) & ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) )
proof
defpred S2[ set , set ] means ( ( for k being Nat st k = $1 & 1 <= k & k <= len p holds
$2 = p . k ) & ( for k being Nat st k = $1 & (len p) + 1 <= k & k <= (len p) + (len q) holds
$2 = q . (k - (len p)) ) );
A1: for x being set st x in Seg ((len p) + (len q)) holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in Seg ((len p) + (len q)) implies ex y being set st S2[x,y] )
assume x in Seg ((len p) + (len q)) ; ::_thesis: ex y being set st S2[x,y]
then reconsider m = x as Element of NAT ;
A2: now__::_thesis:_(_(len_p)_+_1_<=_m_implies_ex_y_being_set_st_S2[x,y]_)
assume A3: (len p) + 1 <= m ; ::_thesis: ex y being set st S2[x,y]
set y = q . (m - (len p));
A4: for k being Nat st k = x & 1 <= k & k <= len p holds
q . (m - (len p)) = p . k
proof
let k be Nat; ::_thesis: ( k = x & 1 <= k & k <= len p implies q . (m - (len p)) = p . k )
assume that
A5: k = x and
1 <= k and
A6: k <= len p ; ::_thesis: q . (m - (len p)) = p . k
m + ((len p) + 1) <= m + (len p) by A3, A5, A6, XREAL_1:7;
then (m + (len p)) + 1 <= (m + (len p)) + 0 ;
hence q . (m - (len p)) = p . k by XREAL_1:6; ::_thesis: verum
end;
for k being Nat st k = x & (len p) + 1 <= k & k <= (len p) + (len q) holds
q . (m - (len p)) = q . (k - (len p)) ;
hence ex y being set st S2[x,y] by A4; ::_thesis: verum
end;
now__::_thesis:_(_not_(len_p)_+_1_<=_m_implies_ex_y_being_set_st_S2[x,y]_)
assume A7: not (len p) + 1 <= m ; ::_thesis: ex y being set st S2[x,y]
set y = p . m;
( ( for k being Nat st k = x & 1 <= k & k <= len p holds
p . m = p . k ) & ( for k being Nat st k = x & (len p) + 1 <= k & k <= (len p) + (len q) holds
p . m = q . (k - (len p)) ) ) by A7;
hence ex y being set st S2[x,y] ; ::_thesis: verum
end;
hence ex y being set st S2[x,y] by A2; ::_thesis: verum
end;
consider f being Function such that
A8: ( dom f = Seg ((len p) + (len q)) & ( for x being set st x in Seg ((len p) + (len q)) holds
S2[x,f . x] ) ) from CLASSES1:sch_1(A1);
A9: for k being Nat st k in dom p holds
f . k = p . k
proof
let k be Nat; ::_thesis: ( k in dom p implies f . k = p . k )
assume k in dom p ; ::_thesis: f . k = p . k
then A10: k in Seg (len p) by Def3;
then A11: ( 1 <= k & k <= len p ) by Th1;
len p <= (len p) + (len q) by NAT_1:11;
then Seg (len p) c= Seg ((len p) + (len q)) by Th5;
hence f . k = p . k by A8, A10, A11; ::_thesis: verum
end;
A12: for n being Nat st n in dom q holds
f . ((len p) + n) = q . n
proof
let n be Nat; ::_thesis: ( n in dom q implies f . ((len p) + n) = q . n )
assume n in dom q ; ::_thesis: f . ((len p) + n) = q . n
then A13: n in Seg (len q) by Def3;
then A14: 1 <= n by Th1;
A15: n <= len q by A13, Th1;
A16: (len p) + 1 <= (len p) + n by A14, XREAL_1:7;
A17: (len p) + n <= (len p) + (len q) by A15, XREAL_1:7;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
(len p) + n <= ((len p) + n) + (len p) by NAT_1:11;
then (len p) + 1 <= ((len p) + n) + (len p) by A16, XXREAL_0:2;
then 1 <= (len p) + n by XREAL_1:6;
then (len p) + n in Seg ((len p) + (len q)) by A17;
then f . ((len p) + n) = q . ((n + (len p)) - (len p)) by A8, A16, A17;
hence f . ((len p) + n) = q . n ; ::_thesis: verum
end;
reconsider r = f as FinSequence by A8, Def2;
take r ; ::_thesis: ( dom r = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
r . k = p . k ) & ( for k being Nat st k in dom q holds
r . ((len p) + k) = q . k ) )
thus ( dom r = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
r . k = p . k ) & ( for k being Nat st k in dom q holds
r . ((len p) + k) = q . k ) ) by A8, A9, A12; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence st dom b1 = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b1 . k = p . k ) & ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) & dom b2 = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b2 . k = p . k ) & ( for k being Nat st k in dom q holds
b2 . ((len p) + k) = q . k ) holds
b1 = b2
proof
let f, g be FinSequence; ::_thesis: ( dom f = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
f . k = p . k ) & ( for k being Nat st k in dom q holds
f . ((len p) + k) = q . k ) & dom g = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
g . k = p . k ) & ( for k being Nat st k in dom q holds
g . ((len p) + k) = q . k ) implies f = g )
assume that
A18: dom f = Seg ((len p) + (len q)) and
A19: for k being Nat st k in dom p holds
f . k = p . k and
A20: for k being Nat st k in dom q holds
f . ((len p) + k) = q . k and
A21: dom g = Seg ((len p) + (len q)) and
A22: for k being Nat st k in dom p holds
g . k = p . k and
A23: for k being Nat st k in dom q holds
g . ((len p) + k) = q . k ; ::_thesis: f = g
for x being set st x in Seg ((len p) + (len q)) holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in Seg ((len p) + (len q)) implies f . x = g . x )
assume A24: x in Seg ((len p) + (len q)) ; ::_thesis: f . x = g . x
then reconsider k = x as Element of NAT ;
A25: 1 <= k by A24, Th1;
A26: now__::_thesis:_(_(len_p)_+_1_<=_k_implies_f_._x_=_g_._x_)
assume (len p) + 1 <= k ; ::_thesis: f . x = g . x
then consider m being Nat such that
A27: ((len p) + 1) + m = k by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
(len p) + (1 + m) <= (len p) + (len q) by A24, A27, Th1;
then ( 1 + 0 <= 1 + m & 1 + m <= len q ) by XREAL_1:6;
then 1 + m in Seg (len q) ;
then A28: 1 + m in dom q by Def3;
then g . ((len p) + (1 + m)) = q . (1 + m) by A23;
hence f . x = g . x by A20, A27, A28; ::_thesis: verum
end;
now__::_thesis:_(_not_(len_p)_+_1_<=_k_implies_f_._x_=_g_._x_)
assume not (len p) + 1 <= k ; ::_thesis: f . x = g . x
then k <= len p by NAT_1:8;
then k in Seg (len p) by A25;
then A29: k in dom p by Def3;
then f . k = p . k by A19;
hence f . x = g . x by A22, A29; ::_thesis: verum
end;
hence f . x = g . x by A26; ::_thesis: verum
end;
hence f = g by A18, A21, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines ^ FINSEQ_1:def_7_:_
for p, q being FinSequence
for b3 being FinSequence holds
( b3 = p ^ q iff ( dom b3 = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b3 . k = p . k ) & ( for k being Nat st k in dom q holds
b3 . ((len p) + k) = q . k ) ) );
theorem Th21: :: FINSEQ_1:21
for p, q being FinSequence holds p = (p ^ q) | (dom p)
proof
let p, q be FinSequence; ::_thesis: p = (p ^ q) | (dom p)
A1: dom (p ^ q) = Seg ((len p) + (len q)) by Def7;
A2: dom p = Seg (len p) by Def3;
then A3: dom p = (dom (p ^ q)) /\ (Seg (len p)) by A1, Th7, NAT_1:12;
for x being set st x in dom p holds
p . x = (p ^ q) . x by Def7;
hence p = (p ^ q) | (dom p) by A2, A3, FUNCT_1:46; ::_thesis: verum
end;
theorem Th22: :: FINSEQ_1:22
for p, q being FinSequence holds len (p ^ q) = (len p) + (len q)
proof
let p, q be FinSequence; ::_thesis: len (p ^ q) = (len p) + (len q)
dom (p ^ q) = Seg ((len p) + (len q)) by Def7;
hence len (p ^ q) = (len p) + (len q) by Def3; ::_thesis: verum
end;
theorem Th23: :: FINSEQ_1:23
for p, q being FinSequence
for k being Nat st (len p) + 1 <= k & k <= (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
proof
let p, q be FinSequence; ::_thesis: for k being Nat st (len p) + 1 <= k & k <= (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
let k be Nat; ::_thesis: ( (len p) + 1 <= k & k <= (len p) + (len q) implies (p ^ q) . k = q . (k - (len p)) )
assume that
A1: (len p) + 1 <= k and
A2: k <= (len p) + (len q) ; ::_thesis: (p ^ q) . k = q . (k - (len p))
consider m being Nat such that
A3: ((len p) + 1) + m = k by A1, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A4: (len p) + (1 + m) = k by A3;
1 + m = k - (len p) by A3;
then A5: 1 <= 1 + m by A1, XREAL_1:19;
k - (len p) <= len q by A2, XREAL_1:20;
then 1 + m in Seg (len q) by A3, A5;
then 1 + m in dom q by Def3;
hence (p ^ q) . k = q . (k - (len p)) by A4, Def7; ::_thesis: verum
end;
theorem Th24: :: FINSEQ_1:24
for p, q being FinSequence
for k being Nat st len p < k & k <= len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
proof
let p, q be FinSequence; ::_thesis: for k being Nat st len p < k & k <= len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
let k be Nat; ::_thesis: ( len p < k & k <= len (p ^ q) implies (p ^ q) . k = q . (k - (len p)) )
assume ( len p < k & k <= len (p ^ q) ) ; ::_thesis: (p ^ q) . k = q . (k - (len p))
then ( (len p) + 1 <= k & k <= (len p) + (len q) ) by Th22, NAT_1:13;
hence (p ^ q) . k = q . (k - (len p)) by Th23; ::_thesis: verum
end;
theorem Th25: :: FINSEQ_1:25
for p, q being FinSequence
for k being Nat holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
proof
let p, q be FinSequence; ::_thesis: for k being Nat holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
let k be Nat; ::_thesis: ( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
assume k in dom (p ^ q) ; ::_thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then A1: k in Seg (len (p ^ q)) by Def3;
then A2: k in Seg ((len p) + (len q)) by Th22;
A3: ( k in NAT & 1 <= k ) by A1, Th1;
A4: now__::_thesis:_(_(len_p)_+_1_<=_k_or_k_in_dom_p_or_ex_n_being_Nat_st_
(_n_in_dom_q_&_k_=_(len_p)_+_n_)_)
assume not (len p) + 1 <= k ; ::_thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then k <= len p by NAT_1:8;
then k in Seg (len p) by A3;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by Def3; ::_thesis: verum
end;
now__::_thesis:_(_not_(len_p)_+_1_<=_k_or_k_in_dom_p_or_ex_n_being_Nat_st_
(_n_in_dom_q_&_k_=_(len_p)_+_n_)_)
assume (len p) + 1 <= k ; ::_thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then consider n being Nat such that
A5: k = ((len p) + 1) + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
(len p) + (1 + n) <= (len p) + (len q) by A2, A5, Th1;
then A6: 1 + n <= len q by XREAL_1:6;
1 <= 1 + n by NAT_1:11;
then 1 + n in Seg (len q) by A6;
then A7: 1 + n in dom q by Def3;
k = (len p) + (1 + n) by A5;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A7; ::_thesis: verum
end;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A4; ::_thesis: verum
end;
theorem Th26: :: FINSEQ_1:26
for p, q being FinSequence holds dom p c= dom (p ^ q)
proof
let p, q be FinSequence; ::_thesis: dom p c= dom (p ^ q)
len p <= (len p) + (len q) by NAT_1:11;
then Seg (len p) c= Seg ((len p) + (len q)) by Th5;
then Seg (len p) c= dom (p ^ q) by Def7;
hence dom p c= dom (p ^ q) by Def3; ::_thesis: verum
end;
theorem Th27: :: FINSEQ_1:27
for x being set
for q, p being FinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
proof
let x be set ; ::_thesis: for q, p being FinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
let q, p be FinSequence; ::_thesis: ( x in dom q implies ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) ) )
assume A1: x in dom q ; ::_thesis: ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
then A2: x in Seg (len q) by Def3;
reconsider k = x as Element of NAT by A1;
take k ; ::_thesis: ( k = x & (len p) + k in dom (p ^ q) )
A3: 1 <= k by A2, Th1;
A4: k <= len q by A2, Th1;
k <= (len p) + k by NAT_1:11;
then A5: 1 <= (len p) + k by A3, XXREAL_0:2;
(len p) + k <= (len p) + (len q) by A4, XREAL_1:7;
then (len p) + k in Seg ((len p) + (len q)) by A5;
hence ( k = x & (len p) + k in dom (p ^ q) ) by Def7; ::_thesis: verum
end;
theorem Th28: :: FINSEQ_1:28
for k being Nat
for q, p being FinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
proof
let k be Nat; ::_thesis: for q, p being FinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
let q, p be FinSequence; ::_thesis: ( k in dom q implies (len p) + k in dom (p ^ q) )
assume k in dom q ; ::_thesis: (len p) + k in dom (p ^ q)
then ex n being Nat st
( n = k & (len p) + n in dom (p ^ q) ) by Th27;
hence (len p) + k in dom (p ^ q) ; ::_thesis: verum
end;
theorem Th29: :: FINSEQ_1:29
for p, q being FinSequence holds rng p c= rng (p ^ q)
proof
let p, q be FinSequence; ::_thesis: rng p c= rng (p ^ q)
now__::_thesis:_for_x_being_set_st_x_in_rng_p_holds_
x_in_rng_(p_^_q)
let x be set ; ::_thesis: ( x in rng p implies x in rng (p ^ q) )
assume x in rng p ; ::_thesis: x in rng (p ^ q)
then consider y being set such that
A1: y in dom p and
A2: x = p . y by FUNCT_1:def_3;
reconsider k = y as Element of NAT by A1;
A3: dom p c= dom (p ^ q) by Th26;
(p ^ q) . k = p . k by A1, Def7;
hence x in rng (p ^ q) by A1, A2, A3, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng p c= rng (p ^ q) by TARSKI:def_3; ::_thesis: verum
end;
theorem Th30: :: FINSEQ_1:30
for q, p being FinSequence holds rng q c= rng (p ^ q)
proof
let q, p be FinSequence; ::_thesis: rng q c= rng (p ^ q)
now__::_thesis:_for_x_being_set_st_x_in_rng_q_holds_
x_in_rng_(p_^_q)
let x be set ; ::_thesis: ( x in rng q implies x in rng (p ^ q) )
assume x in rng q ; ::_thesis: x in rng (p ^ q)
then consider y being set such that
A1: y in dom q and
A2: x = q . y by FUNCT_1:def_3;
reconsider k = y as Element of NAT by A1;
( (len p) + k in dom (p ^ q) & (p ^ q) . ((len p) + k) = q . k ) by A1, Def7, Th28;
hence x in rng (p ^ q) by A2, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng q c= rng (p ^ q) by TARSKI:def_3; ::_thesis: verum
end;
theorem Th31: :: FINSEQ_1:31
for p, q being FinSequence holds rng (p ^ q) = (rng p) \/ (rng q)
proof
let p, q be FinSequence; ::_thesis: rng (p ^ q) = (rng p) \/ (rng q)
now__::_thesis:_for_x_being_set_st_x_in_rng_(p_^_q)_holds_
x_in_(rng_p)_\/_(rng_q)
let x be set ; ::_thesis: ( x in rng (p ^ q) implies x in (rng p) \/ (rng q) )
assume x in rng (p ^ q) ; ::_thesis: x in (rng p) \/ (rng q)
then consider y being set such that
A1: y in dom (p ^ q) and
A2: x = (p ^ q) . y by FUNCT_1:def_3;
A3: y in Seg ((len p) + (len q)) by A1, Def7;
reconsider k = y as Element of NAT by A1;
A4: 1 <= k by A3, Th1;
A5: k <= (len p) + (len q) by A3, Th1;
A6: now__::_thesis:_(_(len_p)_+_1_<=_k_implies_x_in_rng_q_)
assume A7: (len p) + 1 <= k ; ::_thesis: x in rng q
then A8: q . (k - (len p)) = x by A2, A5, Th23;
consider m being Nat such that
A9: ((len p) + 1) + m = k by A7, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
(len p) + (1 + m) = k by A9;
then ( 1 + 0 <= 1 + m & 1 + m <= len q ) by A5, XREAL_1:6;
then 1 + m in Seg (len q) ;
then k - (len p) in dom q by A9, Def3;
hence x in rng q by A8, FUNCT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_not_(len_p)_+_1_<=_k_implies_x_in_rng_p_)
assume not (len p) + 1 <= k ; ::_thesis: x in rng p
then k <= len p by NAT_1:8;
then k in Seg (len p) by A4;
then A10: k in dom p by Def3;
then p . k = x by A2, Def7;
hence x in rng p by A10, FUNCT_1:def_3; ::_thesis: verum
end;
hence x in (rng p) \/ (rng q) by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
then A11: rng (p ^ q) c= (rng p) \/ (rng q) by TARSKI:def_3;
( rng p c= rng (p ^ q) & rng q c= rng (p ^ q) ) by Th29, Th30;
then (rng p) \/ (rng q) c= rng (p ^ q) by XBOOLE_1:8;
hence rng (p ^ q) = (rng p) \/ (rng q) by A11, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th32: :: FINSEQ_1:32
for p, q, r being FinSequence holds (p ^ q) ^ r = p ^ (q ^ r)
proof
let p, q, r be FinSequence; ::_thesis: (p ^ q) ^ r = p ^ (q ^ r)
A1: dom ((p ^ q) ^ r) = Seg ((len (p ^ q)) + (len r)) by Def7
.= Seg (((len p) + (len q)) + (len r)) by Th22
.= Seg ((len p) + ((len q) + (len r)))
.= Seg ((len p) + (len (q ^ r))) by Th22 ;
A2: for k being Nat st k in dom p holds
((p ^ q) ^ r) . k = p . k
proof
let k be Nat; ::_thesis: ( k in dom p implies ((p ^ q) ^ r) . k = p . k )
assume A3: k in dom p ; ::_thesis: ((p ^ q) ^ r) . k = p . k
dom p c= dom (p ^ q) by Th26;
hence ((p ^ q) ^ r) . k = (p ^ q) . k by A3, Def7
.= p . k by A3, Def7 ;
::_thesis: verum
end;
for k being Nat st k in dom (q ^ r) holds
((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
proof
let k be Nat; ::_thesis: ( k in dom (q ^ r) implies ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k )
assume A4: k in dom (q ^ r) ; ::_thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
A5: now__::_thesis:_(_k_in_dom_q_implies_((p_^_q)_^_r)_._((len_p)_+_k)_=_(q_^_r)_._k_)
assume A6: k in dom q ; ::_thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
then (len p) + k in dom (p ^ q) by Th28;
hence ((p ^ q) ^ r) . ((len p) + k) = (p ^ q) . ((len p) + k) by Def7
.= q . k by A6, Def7
.= (q ^ r) . k by A6, Def7 ;
::_thesis: verum
end;
now__::_thesis:_(_not_k_in_dom_q_implies_((p_^_q)_^_r)_._((len_p)_+_k)_=_(q_^_r)_._k_)
assume not k in dom q ; ::_thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
then consider n being Nat such that
A7: n in dom r and
A8: k = (len q) + n by A4, Th25;
thus ((p ^ q) ^ r) . ((len p) + k) = ((p ^ q) ^ r) . (((len p) + (len q)) + n) by A8
.= ((p ^ q) ^ r) . ((len (p ^ q)) + n) by Th22
.= r . n by A7, Def7
.= (q ^ r) . k by A7, A8, Def7 ; ::_thesis: verum
end;
hence ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k by A5; ::_thesis: verum
end;
hence (p ^ q) ^ r = p ^ (q ^ r) by A1, A2, Def7; ::_thesis: verum
end;
theorem :: FINSEQ_1:33
for p, r, q being FinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q
proof
let p, r, q be FinSequence; ::_thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )
assume A1: ( p ^ r = q ^ r or r ^ p = r ^ q ) ; ::_thesis: p = q
A2: now__::_thesis:_(_p_^_r_=_q_^_r_implies_p_=_q_)
assume A3: p ^ r = q ^ r ; ::_thesis: p = q
then (len p) + (len r) = len (q ^ r) by Th22;
then (len p) + (len r) = (len q) + (len r) by Th22;
then A4: dom p = Seg (len q) by Def3
.= dom q by Def3 ;
for k being Nat st k in dom p holds
p . k = q . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = q . k )
assume A5: k in dom p ; ::_thesis: p . k = q . k
hence p . k = (q ^ r) . k by A3, Def7
.= q . k by A4, A5, Def7 ;
::_thesis: verum
end;
hence p = q by A4, Th13; ::_thesis: verum
end;
now__::_thesis:_(_r_^_p_=_r_^_q_implies_p_=_q_)
assume A6: r ^ p = r ^ q ; ::_thesis: p = q
then (len r) + (len p) = len (r ^ q) by Th22
.= (len r) + (len q) by Th22 ;
then A7: dom p = Seg (len q) by Def3
.= dom q by Def3 ;
for k being Nat st k in dom p holds
p . k = q . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = q . k )
assume A8: k in dom p ; ::_thesis: p . k = q . k
hence p . k = (r ^ q) . ((len r) + k) by A6, Def7
.= q . k by A7, A8, Def7 ;
::_thesis: verum
end;
hence p = q by A7, Th13; ::_thesis: verum
end;
hence p = q by A1, A2; ::_thesis: verum
end;
theorem Th34: :: FINSEQ_1:34
for p being FinSequence holds
( p ^ {} = p & {} ^ p = p )
proof
let p be FinSequence; ::_thesis: ( p ^ {} = p & {} ^ p = p )
A1: dom (p ^ {}) = Seg (len (p ^ {})) by Def3
.= Seg ((len p) + (len {})) by Th22
.= dom p by Def3 ;
for k being Nat st k in dom p holds
p . k = (p ^ {}) . k by Def7;
hence p ^ {} = p by A1, Th13; ::_thesis: {} ^ p = p
A2: dom ({} ^ p) = Seg (len ({} ^ p)) by Def3
.= Seg ((len {}) + (len p)) by Th22
.= dom p by Def3 ;
for k being Nat st k in dom p holds
p . k = ({} ^ p) . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = ({} ^ p) . k )
assume A3: k in dom p ; ::_thesis: p . k = ({} ^ p) . k
thus ({} ^ p) . k = ({} ^ p) . ((len {}) + k)
.= p . k by A3, Def7 ; ::_thesis: verum
end;
hence {} ^ p = p by A2, Th13; ::_thesis: verum
end;
theorem Th35: :: FINSEQ_1:35
for p, q being FinSequence st p ^ q = {} holds
( p = {} & q = {} )
proof
let p, q be FinSequence; ::_thesis: ( p ^ q = {} implies ( p = {} & q = {} ) )
assume p ^ q = {} ; ::_thesis: ( p = {} & q = {} )
then 0 = len (p ^ q)
.= (len p) + (len q) by Th22 ;
hence ( p = {} & q = {} ) ; ::_thesis: verum
end;
definition
let D be set ;
let p, q be FinSequence of D;
:: original: ^
redefine funcp ^ q -> FinSequence of D;
coherence
p ^ q is FinSequence of D
proof
A1: ( rng (p ^ q) = (rng p) \/ (rng q) & rng p c= D ) by Def4, Th31;
rng q c= D by Def4;
hence rng (p ^ q) c= D by A1, XBOOLE_1:8; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
end;
Lm5: for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
proof
let x, y be set ; ::_thesis: for x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
let x1, y1 be set ; ::_thesis: ( [x,y] in {[x1,y1]} implies ( x = x1 & y = y1 ) )
assume [x,y] in {[x1,y1]} ; ::_thesis: ( x = x1 & y = y1 )
then [x,y] = [x1,y1] by TARSKI:def_1;
hence ( x = x1 & y = y1 ) by XTUPLE_0:1; ::_thesis: verum
end;
definition
let x be set ;
:: original: <*
redefine func<*x*> -> Function means :Def8: :: FINSEQ_1:def 8
( dom it = Seg 1 & it . 1 = x );
coherence
<*x*> is Function ;
compatibility
for b1 being Function holds
( b1 = <*x*> iff ( dom b1 = Seg 1 & b1 . 1 = x ) )
proof
let f be Function; ::_thesis: ( f = <*x*> iff ( dom f = Seg 1 & f . 1 = x ) )
hereby ::_thesis: ( dom f = Seg 1 & f . 1 = x implies f = <*x*> )
assume A1: f = <*x*> ; ::_thesis: ( dom f = Seg 1 & f . 1 = x )
hence dom f = Seg 1 by Th2, RELAT_1:9; ::_thesis: f . 1 = x
[1,x] in f by A1, TARSKI:def_1;
hence f . 1 = x by FUNCT_1:1; ::_thesis: verum
end;
assume that
A2: dom f = Seg 1 and
A3: f . 1 = x ; ::_thesis: f = <*x*>
reconsider g = {[1,(f . 1)]} as Function ;
for y, z being set holds
( [y,z] in f iff [y,z] in g )
proof
let y, z be set ; ::_thesis: ( [y,z] in f iff [y,z] in g )
hereby ::_thesis: ( [y,z] in g implies [y,z] in f )
assume A4: [y,z] in f ; ::_thesis: [y,z] in g
then A5: y in {1} by A2, Th2, XTUPLE_0:def_12;
A6: z in rng f by A4, XTUPLE_0:def_13;
A7: rng f = {(f . 1)} by A2, Th2, FUNCT_1:4;
A8: y = 1 by A5, TARSKI:def_1;
z = f . 1 by A6, A7, TARSKI:def_1;
hence [y,z] in g by A8, TARSKI:def_1; ::_thesis: verum
end;
assume [y,z] in g ; ::_thesis: [y,z] in f
then A9: ( y = 1 & z = f . 1 ) by Lm5;
1 in dom f by A2;
hence [y,z] in f by A9, FUNCT_1:def_2; ::_thesis: verum
end;
hence f = <*x*> by A3, RELAT_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines <* FINSEQ_1:def_8_:_
for x being set
for b2 being Function holds
( b2 = <*x*> iff ( dom b2 = Seg 1 & b2 . 1 = x ) );
registration
let x be set ;
cluster<*x*> -> Relation-like Function-like ;
coherence
( <*x*> is Function-like & <*x*> is Relation-like ) ;
end;
registration
let x be set ;
cluster<*x*> -> FinSequence-like ;
coherence
<*x*> is FinSequence-like
proof
take 1 ; :: according to FINSEQ_1:def_2 ::_thesis: dom <*x*> = Seg 1
thus dom <*x*> = Seg 1 by Def8; ::_thesis: verum
end;
end;
theorem Th36: :: FINSEQ_1:36
for p, q being FinSequence
for D being set st p ^ q is FinSequence of D holds
( p is FinSequence of D & q is FinSequence of D )
proof
let p, q be FinSequence; ::_thesis: for D being set st p ^ q is FinSequence of D holds
( p is FinSequence of D & q is FinSequence of D )
let D be set ; ::_thesis: ( p ^ q is FinSequence of D implies ( p is FinSequence of D & q is FinSequence of D ) )
assume p ^ q is FinSequence of D ; ::_thesis: ( p is FinSequence of D & q is FinSequence of D )
then rng (p ^ q) c= D by Def4;
then A1: (rng p) \/ (rng q) c= D by Th31;
rng p c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng p c= D by A1, XBOOLE_1:1;
hence p is FinSequence of D by Def4; ::_thesis: q is FinSequence of D
rng q c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng q c= D by A1, XBOOLE_1:1;
hence q is FinSequence of D by Def4; ::_thesis: verum
end;
definition
let x, y be set ;
func<*x,y*> -> set equals :: FINSEQ_1:def 9
<*x*> ^ <*y*>;
correctness
coherence
<*x*> ^ <*y*> is set ;
;
let z be set ;
func<*x,y,z*> -> set equals :: FINSEQ_1:def 10
(<*x*> ^ <*y*>) ^ <*z*>;
correctness
coherence
(<*x*> ^ <*y*>) ^ <*z*> is set ;
;
end;
:: deftheorem defines <* FINSEQ_1:def_9_:_
for x, y being set holds <*x,y*> = <*x*> ^ <*y*>;
:: deftheorem defines <* FINSEQ_1:def_10_:_
for x, y, z being set holds <*x,y,z*> = (<*x*> ^ <*y*>) ^ <*z*>;
registration
let x, y be set ;
cluster<*x,y*> -> Relation-like Function-like ;
coherence
( <*x,y*> is Function-like & <*x,y*> is Relation-like ) ;
let z be set ;
cluster<*x,y,z*> -> Relation-like Function-like ;
coherence
( <*x,y,z*> is Function-like & <*x,y,z*> is Relation-like ) ;
end;
registration
let x, y be set ;
cluster<*x,y*> -> FinSequence-like ;
coherence
<*x,y*> is FinSequence-like ;
let z be set ;
cluster<*x,y,z*> -> FinSequence-like ;
coherence
<*x,y,z*> is FinSequence-like ;
end;
theorem :: FINSEQ_1:37
for x being set holds <*x*> = {[1,x]} ;
theorem Th38: :: FINSEQ_1:38
for x being set
for p being FinSequence holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )
proof
let x be set ; ::_thesis: for p being FinSequence holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )
let p be FinSequence; ::_thesis: ( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )
thus ( p = <*x*> implies ( dom p = Seg 1 & rng p = {x} ) ) ::_thesis: ( dom p = Seg 1 & rng p = {x} implies p = <*x*> )
proof
assume A1: p = <*x*> ; ::_thesis: ( dom p = Seg 1 & rng p = {x} )
hence dom p = Seg 1 by Def8; ::_thesis: rng p = {x}
dom p = {1} by A1, Def8, Th2;
then rng p = {(p . 1)} by FUNCT_1:4;
hence rng p = {x} by A1, Def8; ::_thesis: verum
end;
assume that
A2: dom p = Seg 1 and
A3: rng p = {x} ; ::_thesis: p = <*x*>
1 in dom p by A2;
then p . 1 in {x} by A3, FUNCT_1:def_3;
then p . 1 = x by TARSKI:def_1;
hence p = <*x*> by A2, Def8; ::_thesis: verum
end;
theorem Th39: :: FINSEQ_1:39
for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & rng p = {x} ) )
proof
let x be set ; ::_thesis: for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & rng p = {x} ) )
let p be FinSequence; ::_thesis: ( p = <*x*> iff ( len p = 1 & rng p = {x} ) )
( len p = 1 iff dom p = Seg 1 ) by Def3;
hence ( p = <*x*> iff ( len p = 1 & rng p = {x} ) ) by Th38; ::_thesis: verum
end;
theorem Th40: :: FINSEQ_1:40
for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & p . 1 = x ) )
proof
let x be set ; ::_thesis: for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & p . 1 = x ) )
let p be FinSequence; ::_thesis: ( p = <*x*> iff ( len p = 1 & p . 1 = x ) )
( len p = 1 iff dom p = Seg 1 ) by Def3;
hence ( p = <*x*> iff ( len p = 1 & p . 1 = x ) ) by Def8; ::_thesis: verum
end;
theorem :: FINSEQ_1:41
for x being set
for p being FinSequence holds (<*x*> ^ p) . 1 = x
proof
let x be set ; ::_thesis: for p being FinSequence holds (<*x*> ^ p) . 1 = x
let p be FinSequence; ::_thesis: (<*x*> ^ p) . 1 = x
1 in Seg 1 ;
then 1 in dom <*x*> by Def8;
then (<*x*> ^ p) . 1 = <*x*> . 1 by Def7;
hence (<*x*> ^ p) . 1 = x by Def8; ::_thesis: verum
end;
theorem Th42: :: FINSEQ_1:42
for x being set
for p being FinSequence holds (p ^ <*x*>) . ((len p) + 1) = x
proof
let x be set ; ::_thesis: for p being FinSequence holds (p ^ <*x*>) . ((len p) + 1) = x
let p be FinSequence; ::_thesis: (p ^ <*x*>) . ((len p) + 1) = x
dom <*x*> = Seg 1 by Def8;
then 1 in dom <*x*> ;
hence (p ^ <*x*>) . ((len p) + 1) = <*x*> . 1 by Def7
.= x by Def8 ;
::_thesis: verum
end;
theorem :: FINSEQ_1:43
for x, y, z being set holds
( <*x,y,z*> = <*x*> ^ <*y,z*> & <*x,y,z*> = <*x,y*> ^ <*z*> ) by Th32;
theorem Th44: :: FINSEQ_1:44
for x, y being set
for p being FinSequence holds
( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )
proof
let x, y be set ; ::_thesis: for p being FinSequence holds
( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )
let p be FinSequence; ::_thesis: ( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )
thus ( p = <*x,y*> implies ( len p = 2 & p . 1 = x & p . 2 = y ) ) ::_thesis: ( len p = 2 & p . 1 = x & p . 2 = y implies p = <*x,y*> )
proof
assume A1: p = <*x,y*> ; ::_thesis: ( len p = 2 & p . 1 = x & p . 2 = y )
hence len p = (len <*x*>) + (len <*y*>) by Th22
.= 1 + (len <*y*>) by Th39
.= 1 + 1 by Th39
.= 2 ;
::_thesis: ( p . 1 = x & p . 2 = y )
A2: 1 in {1} by TARSKI:def_1;
then 1 in dom <*x*> by Def8, Th2;
hence p . 1 = <*x*> . 1 by A1, Def7
.= x by Def8 ;
::_thesis: p . 2 = y
A3: 1 in dom <*y*> by A2, Def8, Th2;
thus p . 2 = (<*x*> ^ <*y*>) . (1 + 1) by A1
.= (<*x*> ^ <*y*>) . ((len <*x*>) + 1) by Th39
.= <*y*> . 1 by A3, Def7
.= y by Def8 ; ::_thesis: verum
end;
assume that
A4: len p = 2 and
A5: p . 1 = x and
A6: p . 2 = y ; ::_thesis: p = <*x,y*>
A7: dom p = Seg (1 + 1) by A4, Def3
.= Seg ((len <*x*>) + 1) by Th39
.= Seg ((len <*x*>) + (len <*y*>)) by Th39 ;
A8: for k being Nat st k in dom <*x*> holds
p . k = <*x*> . k
proof
let k be Nat; ::_thesis: ( k in dom <*x*> implies p . k = <*x*> . k )
assume k in dom <*x*> ; ::_thesis: p . k = <*x*> . k
then k in {1} by Def8, Th2;
then k = 1 by TARSKI:def_1;
hence p . k = <*x*> . k by A5, Def8; ::_thesis: verum
end;
for k being Nat st k in dom <*y*> holds
p . ((len <*x*>) + k) = <*y*> . k
proof
let k be Nat; ::_thesis: ( k in dom <*y*> implies p . ((len <*x*>) + k) = <*y*> . k )
assume k in dom <*y*> ; ::_thesis: p . ((len <*x*>) + k) = <*y*> . k
then A9: k in {1} by Def8, Th2;
thus p . ((len <*x*>) + k) = p . (1 + k) by Th39
.= p . (1 + 1) by A9, TARSKI:def_1
.= <*y*> . 1 by A6, Def8
.= <*y*> . k by A9, TARSKI:def_1 ; ::_thesis: verum
end;
hence p = <*x,y*> by A7, A8, Def7; ::_thesis: verum
end;
theorem Th45: :: FINSEQ_1:45
for x, y, z being set
for p being FinSequence holds
( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )
proof
let x, y, z be set ; ::_thesis: for p being FinSequence holds
( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )
let p be FinSequence; ::_thesis: ( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )
thus ( p = <*x,y,z*> implies ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) ) ::_thesis: ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z implies p = <*x,y,z*> )
proof
assume A1: p = <*x,y,z*> ; ::_thesis: ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z )
hence len p = (len <*x,y*>) + (len <*z*>) by Th22
.= 2 + (len <*z*>) by Th44
.= 2 + 1 by Th39
.= 3 ;
::_thesis: ( p . 1 = x & p . 2 = y & p . 3 = z )
A2: 1 in {1} by TARSKI:def_1;
then A3: 1 in dom <*x*> by Def8, Th2;
thus p . 1 = (<*x*> ^ <*y,z*>) . 1 by A1, Th32
.= <*x*> . 1 by A3, Def7
.= x by Def8 ; ::_thesis: ( p . 2 = y & p . 3 = z )
( 2 in Seg 2 & len <*x,y*> = 2 ) by Th44;
then 2 in dom <*x,y*> by Def3;
hence p . 2 = <*x,y*> . 2 by A1, Def7
.= y by Th44 ;
::_thesis: p . 3 = z
A4: 1 in dom <*z*> by A2, Def8, Th2;
thus p . 3 = (<*x,y*> ^ <*z*>) . (2 + 1) by A1
.= (<*x,y*> ^ <*z*>) . ((len <*x,y*>) + 1) by Th44
.= <*z*> . 1 by A4, Def7
.= z by Def8 ; ::_thesis: verum
end;
assume that
A5: len p = 3 and
A6: p . 1 = x and
A7: p . 2 = y and
A8: p . 3 = z ; ::_thesis: p = <*x,y,z*>
A9: dom p = Seg (2 + 1) by A5, Def3
.= Seg ((len <*x,y*>) + 1) by Th44
.= Seg ((len <*x,y*>) + (len <*z*>)) by Th39 ;
A10: for k being Nat st k in dom <*x,y*> holds
p . k = <*x,y*> . k
proof
let k be Nat; ::_thesis: ( k in dom <*x,y*> implies p . k = <*x,y*> . k )
assume A11: k in dom <*x,y*> ; ::_thesis: p . k = <*x,y*> . k
len <*x,y*> = 2 by Th44;
then A12: k in Seg 2 by A11, Def3;
A13: ( k = 1 implies p . k = <*x,y*> . k ) by A6, Th44;
( k = 2 implies p . k = <*x,y*> . k ) by A7, Th44;
hence p . k = <*x,y*> . k by A12, A13, Th2, TARSKI:def_2; ::_thesis: verum
end;
for k being Nat st k in dom <*z*> holds
p . ((len <*x,y*>) + k) = <*z*> . k
proof
let k be Nat; ::_thesis: ( k in dom <*z*> implies p . ((len <*x,y*>) + k) = <*z*> . k )
assume k in dom <*z*> ; ::_thesis: p . ((len <*x,y*>) + k) = <*z*> . k
then k in {1} by Def8, Th2;
then A14: k = 1 by TARSKI:def_1;
hence p . ((len <*x,y*>) + k) = p . (2 + 1) by Th44
.= <*z*> . k by A8, A14, Def8 ;
::_thesis: verum
end;
hence p = <*x,y,z*> by A9, A10, Def7; ::_thesis: verum
end;
theorem Th46: :: FINSEQ_1:46
for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being set st p = q ^ <*x*>
proof
let p be FinSequence; ::_thesis: ( p <> {} implies ex q being FinSequence ex x being set st p = q ^ <*x*> )
assume p <> {} ; ::_thesis: ex q being FinSequence ex x being set st p = q ^ <*x*>
then consider n being Nat such that
A1: len p = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider q = p | (Seg n) as FinSequence by Th15;
take q ; ::_thesis: ex x being set st p = q ^ <*x*>
take p . (len p) ; ::_thesis: p = q ^ <*(p . (len p))*>
A2: dom q = (dom p) /\ (Seg n) by RELAT_1:61
.= (Seg (len p)) /\ (Seg n) by Def3 ;
n <= len p by A1, NAT_1:11;
then Seg n c= Seg (len p) by Th5;
then A3: dom q = Seg n by A2, XBOOLE_1:28;
A4: dom (q ^ <*(p . (len p))*>) = Seg (len (q ^ <*(p . (len p))*>)) by Def3
.= Seg ((len q) + (len <*(p . (len p))*>)) by Th22
.= Seg ((len q) + 1) by Th39
.= Seg (len p) by A1, A3, Def3
.= dom p by Def3 ;
for x being set st x in dom p holds
p . x = (q ^ <*(p . (len p))*>) . x
proof
let x be set ; ::_thesis: ( x in dom p implies p . x = (q ^ <*(p . (len p))*>) . x )
assume A5: x in dom p ; ::_thesis: p . x = (q ^ <*(p . (len p))*>) . x
then reconsider k = x as Element of NAT ;
k in Seg (n + 1) by A1, A5, Def3;
then A6: k in (Seg n) \/ {(n + 1)} by Th9;
A7: now__::_thesis:_(_k_in_Seg_n_implies_p_._k_=_(q_^_<*(p_._(len_p))*>)_._k_)
assume A8: k in Seg n ; ::_thesis: p . k = (q ^ <*(p . (len p))*>) . k
hence p . k = q . k by A3, FUNCT_1:47
.= (q ^ <*(p . (len p))*>) . k by A3, A8, Def7 ;
::_thesis: verum
end;
now__::_thesis:_(_k_in_{(n_+_1)}_implies_(q_^_<*(p_._(len_p))*>)_._k_=_p_._k_)
assume A9: k in {(n + 1)} ; ::_thesis: (q ^ <*(p . (len p))*>) . k = p . k
1 in Seg 1 ;
then A10: 1 in dom <*(p . (len p))*> by Def8;
thus (q ^ <*(p . (len p))*>) . k = (q ^ <*(p . (len p))*>) . (n + 1) by A9, TARSKI:def_1
.= (q ^ <*(p . (len p))*>) . ((len q) + 1) by A3, Def3
.= <*(p . (len p))*> . 1 by A10, Def7
.= p . (n + 1) by A1, Def8
.= p . k by A9, TARSKI:def_1 ; ::_thesis: verum
end;
hence p . x = (q ^ <*(p . (len p))*>) . x by A6, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
hence q ^ <*(p . (len p))*> = p by A4, FUNCT_1:2; ::_thesis: verum
end;
definition
let D be non empty set ;
let x be Element of D;
:: original: <*
redefine func<*x*> -> FinSequence of D;
coherence
<*x*> is FinSequence of D
proof
let y be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not y in rng <*x*> or y in D )
assume y in rng <*x*> ; ::_thesis: y in D
then y in {x} by Th39;
then y = x by TARSKI:def_1;
hence y in D ; ::_thesis: verum
end;
end;
scheme :: FINSEQ_1:sch 3
IndSeq{ P1[ FinSequence] } :
for p being FinSequence holds P1[p]
provided
A1: P1[ {} ] and
A2: for p being FinSequence
for x being set st P1[p] holds
P1[p ^ <*x*>]
proof
let p be FinSequence; ::_thesis: P1[p]
defpred S2[ set ] means for p being FinSequence st len p = $1 holds
P1[p];
consider X being Subset of REAL such that
A3: for x being Real holds
( x in X iff S2[x] ) from SUBSET_1:sch_3();
for k being Nat holds k in X
proof
defpred S3[ Nat] means $1 in X;
for q being FinSequence st len q = 0 holds
P1[q] by A1, Lm4;
then A4: S3[ 0 ] by A3;
now__::_thesis:_for_n_being_Nat_st_n_in_X_holds_
n_+_1_in_X
let n be Nat; ::_thesis: ( n in X implies n + 1 in X )
assume A5: n in X ; ::_thesis: n + 1 in X
now__::_thesis:_for_q_being_FinSequence_st_len_q_=_n_+_1_holds_
P1[q]
let q be FinSequence; ::_thesis: ( len q = n + 1 implies P1[q] )
assume A6: len q = n + 1 ; ::_thesis: P1[q]
then q <> {} ;
then consider r being FinSequence, x being set such that
A7: q = r ^ <*x*> by Th46;
len q = (len r) + (len <*x*>) by A7, Th22
.= (len r) + 1 by Th39 ;
then P1[r] by A3, A5, A6;
hence P1[q] by A2, A7; ::_thesis: verum
end;
hence n + 1 in X by A3; ::_thesis: verum
end;
then A8: for n being Nat st S3[n] holds
S3[n + 1] ;
thus for n being Nat holds S3[n] from NAT_1:sch_2(A4, A8); ::_thesis: verum
end;
then len p in X ;
hence P1[p] by A3; ::_thesis: verum
end;
theorem :: FINSEQ_1:47
for p, q, r, s being FinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being FinSequence st p ^ t = r
proof
defpred S2[ FinSequence] means for p, q, s being FinSequence st p ^ q = $1 ^ s & len p <= len $1 holds
ex t being FinSequence st p ^ t = $1;
A1: S2[ {} ]
proof
let p, q, s be FinSequence; ::_thesis: ( p ^ q = {} ^ s & len p <= len {} implies ex t being FinSequence st p ^ t = {} )
assume that
p ^ q = {} ^ s and
A2: len p <= len {} ; ::_thesis: ex t being FinSequence st p ^ t = {}
take {} ; ::_thesis: p ^ {} = {}
thus p ^ {} = p by Th34
.= {} by A2 ; ::_thesis: verum
end;
A3: for r being FinSequence
for x being set st S2[r] holds
S2[r ^ <*x*>]
proof
let r be FinSequence; ::_thesis: for x being set st S2[r] holds
S2[r ^ <*x*>]
let x be set ; ::_thesis: ( S2[r] implies S2[r ^ <*x*>] )
assume A4: for p, q, s being FinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being FinSequence st p ^ t = r ; ::_thesis: S2[r ^ <*x*>]
let p, q, s be FinSequence; ::_thesis: ( p ^ q = (r ^ <*x*>) ^ s & len p <= len (r ^ <*x*>) implies ex t being FinSequence st p ^ t = r ^ <*x*> )
assume that
A5: p ^ q = (r ^ <*x*>) ^ s and
A6: len p <= len (r ^ <*x*>) ; ::_thesis: ex t being FinSequence st p ^ t = r ^ <*x*>
A7: now__::_thesis:_(_len_p_=_len_(r_^_<*x*>)_implies_ex_t_being_FinSequence_st_p_^_t_=_r_^_<*x*>_)
assume len p = len (r ^ <*x*>) ; ::_thesis: ex t being FinSequence st p ^ t = r ^ <*x*>
then A8: dom p = Seg (len (r ^ <*x*>)) by Def3
.= dom (r ^ <*x*>) by Def3 ;
A9: for k being Nat st k in dom p holds
p . k = (r ^ <*x*>) . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = (r ^ <*x*>) . k )
assume A10: k in dom p ; ::_thesis: p . k = (r ^ <*x*>) . k
hence p . k = ((r ^ <*x*>) ^ s) . k by A5, Def7
.= (r ^ <*x*>) . k by A8, A10, Def7 ;
::_thesis: verum
end;
p ^ {} = p by Th34
.= r ^ <*x*> by A8, A9, Th13 ;
hence ex t being FinSequence st p ^ t = r ^ <*x*> ; ::_thesis: verum
end;
now__::_thesis:_(_len_p_<>_len_(r_^_<*x*>)_implies_ex_t_being_FinSequence_st_p_^_t_=_r_^_<*x*>_)
assume len p <> len (r ^ <*x*>) ; ::_thesis: ex t being FinSequence st p ^ t = r ^ <*x*>
then len p <> (len r) + (len <*x*>) by Th22;
then A11: len p <> (len r) + 1 by Th39;
len p <= (len r) + (len <*x*>) by A6, Th22;
then A12: len p <= (len r) + 1 by Th39;
p ^ q = r ^ (<*x*> ^ s) by A5, Th32;
then consider t being FinSequence such that
A13: p ^ t = r by A4, A11, A12, NAT_1:8;
p ^ (t ^ <*x*>) = r ^ <*x*> by A13, Th32;
hence ex t being FinSequence st p ^ t = r ^ <*x*> ; ::_thesis: verum
end;
hence ex t being FinSequence st p ^ t = r ^ <*x*> by A7; ::_thesis: verum
end;
for r being FinSequence holds S2[r] from FINSEQ_1:sch_3(A1, A3);
hence for p, q, r, s being FinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being FinSequence st p ^ t = r ; ::_thesis: verum
end;
registration
cluster Relation-like Function-like FinSequence-like -> NAT -defined for set ;
coherence
for b1 being FinSequence holds b1 is NAT -defined
proof
let f be FinSequence; ::_thesis: f is NAT -defined
thus dom f c= NAT ; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;
definition
let D be set ;
funcD * -> set means :Def11: :: FINSEQ_1:def 11
for x being set holds
( x in it iff x is FinSequence of D );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is FinSequence of D )
proof
defpred S2[ set ] means $1 is FinSequence of D;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool [:NAT,D:] & S2[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff x is FinSequence of D )
let x be set ; ::_thesis: ( x in X iff x is FinSequence of D )
thus ( x in X implies x is FinSequence of D ) by A1; ::_thesis: ( x is FinSequence of D implies x in X )
assume x is FinSequence of D ; ::_thesis: x in X
then reconsider p = x as FinSequence of D ;
p c= [:NAT,D:] ;
hence x in X by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is FinSequence of D ) ) & ( for x being set holds
( x in b2 iff x is FinSequence of D ) ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( ( for x being set holds
( x in D1 iff x is FinSequence of D ) ) & ( for x being set holds
( x in D2 iff x is FinSequence of D ) ) implies D1 = D2 )
assume that
A2: for x being set holds
( x in D1 iff x is FinSequence of D ) and
A3: for x being set holds
( x in D2 iff x is FinSequence of D ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_D1_implies_x_in_D2_)_&_(_x_in_D2_implies_x_in_D1_)_)
let x be set ; ::_thesis: ( ( x in D1 implies x in D2 ) & ( x in D2 implies x in D1 ) )
thus ( x in D1 implies x in D2 ) ::_thesis: ( x in D2 implies x in D1 )
proof
assume x in D1 ; ::_thesis: x in D2
then x is FinSequence of D by A2;
hence x in D2 by A3; ::_thesis: verum
end;
assume x in D2 ; ::_thesis: x in D1
then x is FinSequence of D by A3;
hence x in D1 by A2; ::_thesis: verum
end;
hence D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines * FINSEQ_1:def_11_:_
for D, b2 being set holds
( b2 = D * iff for x being set holds
( x in b2 iff x is FinSequence of D ) );
registration
let D be set ;
clusterD * -> non empty ;
coherence
not D * is empty
proof
set f = the FinSequence of D;
the FinSequence of D in D * by Def11;
hence not D * is empty ; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:48
for p, q being FinSequence st rng p = rng q & p is one-to-one & q is one-to-one holds
len p = len q
proof
let p, q be FinSequence; ::_thesis: ( rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q )
defpred S2[ FinSequence] means ( $1 is one-to-one implies for q being FinSequence st rng $1 = rng q & q is one-to-one holds
len $1 = len q );
A1: S2[ {} ] by RELAT_1:41;
now__::_thesis:_for_p_being_FinSequence
for_x_being_set_st_(_p_is_one-to-one_implies_for_q_being_FinSequence_st_rng_p_=_rng_q_&_q_is_one-to-one_holds_
len_p_=_len_q_)_&_p_^_<*x*>_is_one-to-one_holds_
for_q_being_FinSequence_st_rng_(p_^_<*x*>)_=_rng_q_&_q_is_one-to-one_holds_
len_(p_^_<*x*>)_=_len_q
let p be FinSequence; ::_thesis: for x being set st ( p is one-to-one implies for q being FinSequence st rng p = rng q & q is one-to-one holds
len p = len q ) & p ^ <*x*> is one-to-one holds
for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len q
let x be set ; ::_thesis: ( ( p is one-to-one implies for q being FinSequence st rng p = rng q & q is one-to-one holds
len p = len q ) & p ^ <*x*> is one-to-one implies for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len q )
assume A2: ( p is one-to-one implies for q being FinSequence st rng p = rng q & q is one-to-one holds
len p = len q ) ; ::_thesis: ( p ^ <*x*> is one-to-one implies for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len q )
assume A3: p ^ <*x*> is one-to-one ; ::_thesis: for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len q
let q be FinSequence; ::_thesis: ( rng (p ^ <*x*>) = rng q & q is one-to-one implies len (p ^ <*x*>) = len q )
assume that
A4: rng (p ^ <*x*>) = rng q and
A5: q is one-to-one ; ::_thesis: len (p ^ <*x*>) = len q
A6: rng (p ^ <*x*>) = (rng p) \/ (rng <*x*>) by Th31
.= (rng p) \/ {x} by Th38 ;
x in {x} by TARSKI:def_1;
then x in rng q by A4, A6, XBOOLE_0:def_3;
then consider y being set such that
A7: y in dom q and
A8: x = q . y by FUNCT_1:def_3;
A9: y in Seg (len q) by A7, Def3;
reconsider y = y as Element of NAT by A7;
A10: 1 <= y by A9, Th1;
then consider k being Nat such that
A11: 1 + k = y by NAT_1:10;
A12: y <= len q by A9, Th1;
then consider n being Nat such that
A13: y + n = len q by NAT_1:10;
reconsider k = k, n = n as Element of NAT by ORDINAL1:def_12;
reconsider q1 = q | (Seg k) as FinSequence by Th15;
defpred S3[ Nat, set ] means $2 = q . (y + $1);
A14: for j being Nat st j in Seg n holds
ex x being set st S3[j,x] ;
consider q2 being FinSequence such that
A15: dom q2 = Seg n and
A16: for j being Nat st j in Seg n holds
S3[j,q2 . j] from FINSEQ_1:sch_1(A14);
k <= y by A11, NAT_1:12;
then A17: k <= len q by A12, XXREAL_0:2;
then A18: len q1 = k by Th17;
(len (q1 ^ <*x*>)) + (len q2) = ((len q1) + (len <*x*>)) + (len q2) by Th22
.= (k + 1) + (len q2) by A18, Th39
.= len q by A11, A13, A15, Def3 ;
then A19: dom q = Seg ((len (q1 ^ <*x*>)) + (len q2)) by Def3;
A20: rng (q1 ^ q2) = (rng q) \ {x}
proof
thus rng (q1 ^ q2) c= (rng q) \ {x} :: according to XBOOLE_0:def_10 ::_thesis: (rng q) \ {x} c= rng (q1 ^ q2)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (q1 ^ q2) or z in (rng q) \ {x} )
assume z in rng (q1 ^ q2) ; ::_thesis: z in (rng q) \ {x}
then A21: z in (rng q1) \/ (rng q2) by Th31;
A22: now__::_thesis:_(_z_in_rng_q1_implies_z_in_(rng_q)_\_{x}_)
assume A23: z in rng q1 ; ::_thesis: z in (rng q) \ {x}
A24: ( rng q1 = q .: (Seg k) & q .: (Seg k) c= rng q ) by RELAT_1:111, RELAT_1:115;
consider y1 being set such that
A25: y1 in dom q1 and
A26: q1 . y1 = z by A23, FUNCT_1:def_3;
A27: q1 . y1 = q . y1 by A25, FUNCT_1:47;
A28: y1 in Seg (len q1) by A25, Def3;
reconsider y1 = y1 as Element of NAT by A25;
A29: y1 <= k by A18, A28, Th1;
A30: k < y by A11, XREAL_1:29;
Seg k c= Seg (len q) by A17, Th5;
then dom q1 c= Seg (len q) by A17, Th17;
then dom q1 c= dom q by Def3;
then x <> z by A5, A7, A8, A25, A26, A27, A29, A30, FUNCT_1:def_4;
then not z in {x} by TARSKI:def_1;
hence z in (rng q) \ {x} by A23, A24, XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_(_z_in_rng_q2_implies_z_in_(rng_q)_\_{x}_)
assume z in rng q2 ; ::_thesis: z in (rng q) \ {x}
then consider y1 being set such that
A31: y1 in dom q2 and
A32: q2 . y1 = z by FUNCT_1:def_3;
reconsider y1 = y1 as Element of NAT by A31;
A33: q2 . y1 = q . (y + y1) by A15, A16, A31;
A34: 1 <= y + y1 by A10, NAT_1:12;
y1 <= n by A15, A31, Th1;
then y + y1 <= len q by A13, XREAL_1:7;
then y + y1 in Seg (len q) by A34;
then A35: y + y1 in dom q by Def3;
then A36: z in rng q by A32, A33, FUNCT_1:def_3;
y1 <> 0 by A15, A31, Th1;
then y <> y + y1 ;
then x <> z by A5, A7, A8, A32, A33, A35, FUNCT_1:def_4;
then not z in {x} by TARSKI:def_1;
hence z in (rng q) \ {x} by A36, XBOOLE_0:def_5; ::_thesis: verum
end;
hence z in (rng q) \ {x} by A21, A22, XBOOLE_0:def_3; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (rng q) \ {x} or z in rng (q1 ^ q2) )
assume A37: z in (rng q) \ {x} ; ::_thesis: z in rng (q1 ^ q2)
then consider y1 being set such that
A38: y1 in dom q and
A39: z = q . y1 by FUNCT_1:def_3;
A40: y1 in Seg (len q) by A38, Def3;
reconsider y1 = y1 as Element of NAT by A38;
not z in {x} by A37, XBOOLE_0:def_5;
then A41: y <> y1 by A8, A39, TARSKI:def_1;
A42: now__::_thesis:_(_y_<_y1_implies_z_in_rng_q2_)
assume A43: y < y1 ; ::_thesis: z in rng q2
then consider j being Nat such that
A44: y1 = y + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A45: 1 <= j by A43, A44, NAT_1:19;
y + j <= len q by A40, A44, Th1;
then j <= n by A13, XREAL_1:6;
then A46: j in Seg n by A45;
then z = q2 . j by A16, A39, A44;
hence z in rng q2 by A15, A46, FUNCT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_y1_<_y_implies_z_in_rng_q1_)
assume A47: y1 < y ; ::_thesis: z in rng q1
A48: 1 <= y1 by A40, Th1;
y1 <= k by A11, A47, NAT_1:13;
then y1 in Seg k by A48;
then A49: y1 in dom q1 by A17, Th17;
then q1 . y1 = z by A39, FUNCT_1:47;
hence z in rng q1 by A49, FUNCT_1:def_3; ::_thesis: verum
end;
then z in (rng q1) \/ (rng q2) by A41, A42, XBOOLE_0:def_3, XXREAL_0:1;
hence z in rng (q1 ^ q2) by Th31; ::_thesis: verum
end;
A50: p = (p ^ <*x*>) | (dom p) by Th21;
A51: rng p = (rng (p ^ <*x*>)) \ {x}
proof
thus rng p c= (rng (p ^ <*x*>)) \ {x} :: according to XBOOLE_0:def_10 ::_thesis: (rng (p ^ <*x*>)) \ {x} c= rng p
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in (rng (p ^ <*x*>)) \ {x} )
assume A52: z in rng p ; ::_thesis: z in (rng (p ^ <*x*>)) \ {x}
A53: rng p c= rng (p ^ <*x*>) by A50, RELAT_1:70;
consider y1 being set such that
A54: y1 in dom p and
A55: p . y1 = z by A52, FUNCT_1:def_3;
A56: y1 in Seg (len p) by A54, Def3;
reconsider y1 = y1 as Element of NAT by A54;
A57: (p ^ <*x*>) . ((len p) + 1) = x by Th42;
A58: (p ^ <*x*>) . y1 = p . y1 by A50, A54, FUNCT_1:47;
A59: y1 <= len p by A56, Th1;
A60: len p < (len p) + 1 by XREAL_1:29;
A61: 1 <= y1 by A56, Th1;
y1 <= (len p) + 1 by A59, A60, XXREAL_0:2;
then A62: y1 in Seg ((len p) + 1) by A61;
A63: (len p) + 1 in Seg ((len p) + 1) by Th3;
A64: y1 in Seg ((len p) + (len <*x*>)) by A62, Th40;
A65: (len p) + 1 in Seg ((len p) + (len <*x*>)) by A63, Th40;
A66: y1 in dom (p ^ <*x*>) by A64, Def7;
(len p) + 1 in dom (p ^ <*x*>) by A65, Def7;
then x <> z by A3, A55, A57, A58, A59, A60, A66, FUNCT_1:def_4;
then not z in {x} by TARSKI:def_1;
hence z in (rng (p ^ <*x*>)) \ {x} by A52, A53, XBOOLE_0:def_5; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (rng (p ^ <*x*>)) \ {x} or z in rng p )
assume A67: z in (rng (p ^ <*x*>)) \ {x} ; ::_thesis: z in rng p
then A68: z in rng (p ^ <*x*>) ;
A69: not z in {x} by A67, XBOOLE_0:def_5;
z in (rng p) \/ (rng <*x*>) by A68, Th31;
then ( z in rng p or z in rng <*x*> ) by XBOOLE_0:def_3;
hence z in rng p by A69, Th38; ::_thesis: verum
end;
A70: q1 ^ q2 is one-to-one
proof
let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y1 in dom (q1 ^ q2) or not b1 in dom (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . b1 or y1 = b1 )
let y2 be set ; ::_thesis: ( not y1 in dom (q1 ^ q2) or not y2 in dom (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . y2 or y1 = y2 )
assume that
A71: ( y1 in dom (q1 ^ q2) & y2 in dom (q1 ^ q2) ) and
A72: (q1 ^ q2) . y1 = (q1 ^ q2) . y2 ; ::_thesis: y1 = y2
reconsider m1 = y1, m2 = y2 as Element of NAT by A71;
A73: q1 is one-to-one by A5, FUNCT_1:52;
A74: now__::_thesis:_(_m1_in_dom_q1_&_m2_in_dom_q1_implies_y1_=_y2_)
assume A75: ( m1 in dom q1 & m2 in dom q1 ) ; ::_thesis: y1 = y2
then ( (q1 ^ q2) . m1 = q1 . m1 & (q1 ^ q2) . m2 = q1 . m2 ) by Def7;
hence y1 = y2 by A72, A73, A75, FUNCT_1:def_4; ::_thesis: verum
end;
A76: now__::_thesis:_(_m1_in_dom_q1_&_ex_j_being_Nat_st_
(_j_in_dom_q2_&_m2_=_(len_q1)_+_j_)_implies_y1_=_y2_)
assume A77: m1 in dom q1 ; ::_thesis: ( ex j being Nat st
( j in dom q2 & m2 = (len q1) + j ) implies y1 = y2 )
given j being Nat such that A78: j in dom q2 and
A79: m2 = (len q1) + j ; ::_thesis: y1 = y2
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A80: (q1 ^ q2) . m2 = q2 . j by A78, A79, Def7;
( (q1 ^ q2) . m1 = q1 . m1 & q1 . m1 = q . m1 ) by A77, Def7, FUNCT_1:47;
then A81: q . m1 = q . (y + j) by A15, A16, A72, A78, A80;
1 <= j by A15, A78, Th1;
then A82: 1 <= y + j by NAT_1:12;
j <= n by A15, A78, Th1;
then y + j <= len q by A13, XREAL_1:7;
then y + j in Seg (len q) by A82;
then A83: y + j in dom q by Def3;
m1 in Seg k by A17, A77, Th17;
then A84: m1 <= k by Th1;
k < y by A11, XREAL_1:29;
then A85: m1 < y by A84, XXREAL_0:2;
( dom q1 c= dom q & y <= y + j ) by NAT_1:12, RELAT_1:60;
hence y1 = y2 by A5, A77, A81, A83, A85, FUNCT_1:def_4; ::_thesis: verum
end;
A86: now__::_thesis:_(_m2_in_dom_q1_&_ex_j_being_Nat_st_
(_j_in_dom_q2_&_m1_=_(len_q1)_+_j_)_implies_y1_=_y2_)
assume A87: m2 in dom q1 ; ::_thesis: ( ex j being Nat st
( j in dom q2 & m1 = (len q1) + j ) implies y1 = y2 )
given j being Nat such that A88: j in dom q2 and
A89: m1 = (len q1) + j ; ::_thesis: y1 = y2
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A90: (q1 ^ q2) . m1 = q2 . j by A88, A89, Def7;
( (q1 ^ q2) . m2 = q1 . m2 & q1 . m2 = q . m2 ) by A87, Def7, FUNCT_1:47;
then A91: q . m2 = q . (y + j) by A15, A16, A72, A88, A90;
1 <= j by A15, A88, Th1;
then A92: 1 <= y + j by NAT_1:12;
j <= n by A15, A88, Th1;
then y + j <= len q by A13, XREAL_1:7;
then y + j in Seg (len q) by A92;
then A93: y + j in dom q by Def3;
m2 in Seg k by A17, A87, Th17;
then A94: m2 <= k by Th1;
k < y by A11, XREAL_1:29;
then A95: m2 < y by A94, XXREAL_0:2;
( dom q1 c= dom q & y <= y + j ) by NAT_1:12, RELAT_1:60;
hence y1 = y2 by A5, A87, A91, A93, A95, FUNCT_1:def_4; ::_thesis: verum
end;
now__::_thesis:_(_ex_j1_being_Nat_st_
(_j1_in_dom_q2_&_m1_=_(len_q1)_+_j1_)_&_ex_j2_being_Nat_st_
(_j2_in_dom_q2_&_m2_=_(len_q1)_+_j2_)_implies_y1_=_y2_)
given j1 being Nat such that A96: j1 in dom q2 and
A97: m1 = (len q1) + j1 ; ::_thesis: ( ex j2 being Nat st
( j2 in dom q2 & m2 = (len q1) + j2 ) implies y1 = y2 )
given j2 being Nat such that A98: j2 in dom q2 and
A99: m2 = (len q1) + j2 ; ::_thesis: y1 = y2
reconsider j1 = j1, j2 = j2 as Element of NAT by ORDINAL1:def_12;
A100: (q1 ^ q2) . m1 = q2 . j1 by A96, A97, Def7;
A101: (q1 ^ q2) . m2 = q2 . j2 by A98, A99, Def7;
A102: (q1 ^ q2) . m1 = q . (y + j1) by A15, A16, A96, A100;
A103: (q1 ^ q2) . m2 = q . (y + j2) by A15, A16, A98, A101;
A104: 1 <= j1 by A15, A96, Th1;
A105: 1 <= j2 by A15, A98, Th1;
A106: 1 <= y + j1 by A104, NAT_1:12;
A107: 1 <= y + j2 by A105, NAT_1:12;
A108: j1 <= n by A15, A96, Th1;
A109: j2 <= n by A15, A98, Th1;
A110: y + j1 <= len q by A13, A108, XREAL_1:7;
A111: y + j2 <= len q by A13, A109, XREAL_1:7;
A112: y + j1 in Seg (len q) by A106, A110;
A113: y + j2 in Seg (len q) by A107, A111;
A114: y + j1 in dom q by A112, Def3;
y + j2 in dom q by A113, Def3;
then y + j1 = y + j2 by A5, A72, A102, A103, A114, FUNCT_1:def_4;
hence y1 = y2 by A97, A99; ::_thesis: verum
end;
hence y1 = y2 by A71, A74, A76, A86, Th25; ::_thesis: verum
end;
A115: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(q1_^_<*x*>)_holds_
q_._j_=_(q1_^_<*x*>)_._j
let j be Nat; ::_thesis: ( j in dom (q1 ^ <*x*>) implies q . j = (q1 ^ <*x*>) . j )
assume A116: j in dom (q1 ^ <*x*>) ; ::_thesis: q . j = (q1 ^ <*x*>) . j
A117: now__::_thesis:_(_j_in_dom_q1_implies_q_._j_=_(q1_^_<*x*>)_._j_)
assume A118: j in dom q1 ; ::_thesis: q . j = (q1 ^ <*x*>) . j
then (q1 ^ <*x*>) . j = q1 . j by Def7;
hence q . j = (q1 ^ <*x*>) . j by A118, FUNCT_1:47; ::_thesis: verum
end;
now__::_thesis:_(_ex_i_being_Nat_st_
(_i_in_dom_<*x*>_&_j_=_(len_q1)_+_i_)_implies_q_._j_=_(q1_^_<*x*>)_._j_)
given i being Nat such that A119: i in dom <*x*> and
A120: j = (len q1) + i ; ::_thesis: q . j = (q1 ^ <*x*>) . j
i in {1} by A119, Th2, Th38;
then i = 1 by TARSKI:def_1;
hence q . j = (q1 ^ <*x*>) . j by A8, A11, A18, A120, Th42; ::_thesis: verum
end;
hence q . j = (q1 ^ <*x*>) . j by A116, A117, Th25; ::_thesis: verum
end;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_q2_holds_
q2_._j_=_q_._((len_(q1_^_<*x*>))_+_j)
let j be Nat; ::_thesis: ( j in dom q2 implies q2 . j = q . ((len (q1 ^ <*x*>)) + j) )
assume j in dom q2 ; ::_thesis: q2 . j = q . ((len (q1 ^ <*x*>)) + j)
hence q2 . j = q . (((len q1) + 1) + j) by A11, A15, A16, A18
.= q . (((len q1) + (len <*x*>)) + j) by Th39
.= q . ((len (q1 ^ <*x*>)) + j) by Th22 ;
::_thesis: verum
end;
then (q1 ^ <*x*>) ^ q2 = q by A19, A115, Def7;
then A121: len q = (len (q1 ^ <*x*>)) + (len q2) by Th22
.= ((len <*x*>) + (len q1)) + (len q2) by Th22
.= (1 + (len q1)) + (len q2) by Th40
.= 1 + ((len q1) + (len q2))
.= (len (q1 ^ q2)) + 1 by Th22 ;
len (p ^ <*x*>) = (len p) + (len <*x*>) by Th22
.= (len p) + 1 by Th40 ;
hence len (p ^ <*x*>) = len q by A2, A3, A4, A20, A50, A51, A70, A121, FUNCT_1:52; ::_thesis: verum
end;
then A122: for p being FinSequence
for x being set st S2[p] holds
S2[p ^ <*x*>] ;
for p being FinSequence holds S2[p] from FINSEQ_1:sch_3(A1, A122);
hence ( rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q ) ; ::_thesis: verum
end;
theorem :: FINSEQ_1:49
for D being set holds {} in D *
proof
let D be set ; ::_thesis: {} in D *
{} = <*> D ;
hence {} in D * by Def11; ::_thesis: verum
end;
scheme :: FINSEQ_1:sch 4
SepSeq{ F1() -> non empty set , P1[ FinSequence] } :
ex X being set st
for x being set holds
( x in X iff ex p being FinSequence st
( p in F1() * & P1[p] & x = p ) )
proof
defpred S2[ set ] means ex p being FinSequence st
( P1[p] & $1 = p );
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in F1() * & S2[x] ) ) from XBOOLE_0:sch_1();
take Y ; ::_thesis: for x being set holds
( x in Y iff ex p being FinSequence st
( p in F1() * & P1[p] & x = p ) )
for x being set holds
( x in Y iff ex p being FinSequence st
( p in F1() * & P1[p] & x = p ) )
proof
let x be set ; ::_thesis: ( x in Y iff ex p being FinSequence st
( p in F1() * & P1[p] & x = p ) )
now__::_thesis:_(_x_in_Y_implies_ex_p_being_FinSequence_st_
(_p_in_F1()_*_&_P1[p]_&_x_=_p_)_)
assume x in Y ; ::_thesis: ex p being FinSequence st
( p in F1() * & P1[p] & x = p )
then ( x in F1() * & ex p being FinSequence st
( P1[p] & x = p ) ) by A1;
hence ex p being FinSequence st
( p in F1() * & P1[p] & x = p ) ; ::_thesis: verum
end;
hence ( x in Y iff ex p being FinSequence st
( p in F1() * & P1[p] & x = p ) ) by A1; ::_thesis: verum
end;
hence for x being set holds
( x in Y iff ex p being FinSequence st
( p in F1() * & P1[p] & x = p ) ) ; ::_thesis: verum
end;
definition
let IT be Function;
attrIT is FinSubsequence-like means :Def12: :: FINSEQ_1:def 12
ex k being Nat st dom IT c= Seg k;
end;
:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def_12_:_
for IT being Function holds
( IT is FinSubsequence-like iff ex k being Nat st dom IT c= Seg k );
registration
cluster Relation-like Function-like FinSubsequence-like for set ;
existence
ex b1 being Function st b1 is FinSubsequence-like
proof
take {} ; ::_thesis: {} is FinSubsequence-like
take len {} ; :: according to FINSEQ_1:def_12 ::_thesis: dom {} c= Seg (len {})
thus dom {} c= Seg (len {}) ; ::_thesis: verum
end;
end;
definition
mode FinSubsequence is FinSubsequence-like Function;
end;
registration
cluster Relation-like Function-like FinSequence-like -> FinSubsequence-like for set ;
coherence
for b1 being Function st b1 is FinSequence-like holds
b1 is FinSubsequence-like
proof
let p be Function; ::_thesis: ( p is FinSequence-like implies p is FinSubsequence-like )
assume p is FinSequence-like ; ::_thesis: p is FinSubsequence-like
then reconsider p = p as FinSequence ;
dom p = Seg (len p) by Def3;
hence p is FinSubsequence-like by Def12; ::_thesis: verum
end;
let p be FinSubsequence;
let X be set ;
clusterp | X -> FinSubsequence-like ;
coherence
p | X is FinSubsequence-like
proof
consider k being Nat such that
A1: dom p c= Seg k by Def12;
dom (p | X) c= dom p by RELAT_1:60;
then dom (p | X) c= Seg k by A1, XBOOLE_1:1;
hence p | X is FinSubsequence-like by Def12; ::_thesis: verum
end;
clusterX |` p -> FinSubsequence-like ;
coherence
X |` p is FinSubsequence-like
proof
consider k being Nat such that
A2: dom p c= Seg k by Def12;
dom (X |` p) c= dom p by FUNCT_1:56;
then dom (X |` p) c= Seg k by A2, XBOOLE_1:1;
hence X |` p is FinSubsequence-like by Def12; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like FinSubsequence-like -> NAT -defined for set ;
coherence
for b1 being FinSubsequence holds b1 is NAT -defined
proof
let f be FinSubsequence; ::_thesis: f is NAT -defined
ex n being Nat st dom f c= Seg n by Def12;
hence dom f c= NAT by XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;
definition
let X be set ;
given k being Nat such that A1: X c= Seg k ;
func Sgm X -> FinSequence of NAT means :Def13: :: FINSEQ_1:def 13
( rng it = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len it & k1 = it . l & k2 = it . m holds
k1 < k2 ) );
existence
ex b1 being FinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
proof
defpred S2[ Nat] means for X being set st X c= Seg $1 holds
ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) );
A2: S2[ 0 ]
proof
let X be set ; ::_thesis: ( X c= Seg 0 implies ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A3: X c= Seg 0 ; ::_thesis: ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
take <*> NAT ; ::_thesis: ( rng (<*> NAT) = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (<*> NAT) & k1 = (<*> NAT) . l & k2 = (<*> NAT) . m holds
k1 < k2 ) )
thus rng (<*> NAT) = X by A3; ::_thesis: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (<*> NAT) & k1 = (<*> NAT) . l & k2 = (<*> NAT) . m holds
k1 < k2
thus for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (<*> NAT) & k1 = (<*> NAT) . l & k2 = (<*> NAT) . m holds
k1 < k2 ; ::_thesis: verum
end;
A4: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A5: for X being set st X c= Seg k holds
ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) ; ::_thesis: S2[k + 1]
let X be set ; ::_thesis: ( X c= Seg (k + 1) implies ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A6: X c= Seg (k + 1) ; ::_thesis: ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
now__::_thesis:_(_not_X_c=_Seg_k_implies_ex_p_being_FinSequence_of_NAT_st_
(_rng_p_=_X_&_(_for_l,_m,_k1,_k2_being_Nat_st_1_<=_l_&_l_<_m_&_m_<=_len_p_&_k1_=_p_._l_&_k2_=_p_._m_holds_
k1_<_k2_)_)_)
assume not X c= Seg k ; ::_thesis: ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
then consider x being set such that
A7: x in X and
A8: not x in Seg k by TARSKI:def_3;
x in Seg (k + 1) by A6, A7;
then reconsider n = x as Element of NAT ;
A9: n = k + 1
proof
assume A10: n <> k + 1 ; ::_thesis: contradiction
A11: n <= k + 1 by A6, A7, Th1;
A12: 1 <= n by A6, A7, Th1;
n <= k by A10, A11, NAT_1:8;
hence contradiction by A8, A12; ::_thesis: verum
end;
set Y = X \ {(k + 1)};
A13: X \ {(k + 1)} c= Seg k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ {(k + 1)} or x in Seg k )
assume A14: x in X \ {(k + 1)} ; ::_thesis: x in Seg k
then A15: x in X ;
A16: not x in {(k + 1)} by A14, XBOOLE_0:def_5;
A17: x in Seg (k + 1) by A6, A15;
A18: x <> k + 1 by A16, TARSKI:def_1;
reconsider m = x as Element of NAT by A17;
A19: m <= k + 1 by A6, A15, Th1;
A20: 1 <= m by A6, A15, Th1;
m <= k by A18, A19, NAT_1:8;
hence x in Seg k by A20; ::_thesis: verum
end;
then consider p being FinSequence of NAT such that
A21: rng p = X \ {(k + 1)} and
A22: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 by A5;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
consider q being FinSequence such that
A23: q = p ^ <*(k + 1)*> ;
reconsider q = q as FinSequence of NAT by A23;
A24: {(k + 1)} c= X by A7, A9, ZFMISC_1:31;
A25: rng q = (rng p) \/ (rng <*(k + 1)*>) by A23, Th31
.= (X \ {(k + 1)}) \/ {(k + 1)} by A21, Th38
.= X \/ {(k + 1)} by XBOOLE_1:39
.= X by A24, XBOOLE_1:12 ;
for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2
proof
let l, m, k1, k2 be Nat; ::_thesis: ( 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m implies k1 < k2 )
assume that
A26: 1 <= l and
A27: l < m and
A28: m <= len q and
A29: k1 = q . l and
A30: k2 = q . m ; ::_thesis: k1 < k2
l < len (p ^ <*(k + 1)*>) by A23, A27, A28, XXREAL_0:2;
then l < (len p) + (len <*(k + 1)*>) by Th22;
then l < (len p) + 1 by Th39;
then l <= len p by NAT_1:13;
then l in Seg (len p) by A26, Th1;
then A31: l in dom p by Def3;
A32: 1 <= m by A26, A27, XXREAL_0:2;
A33: now__::_thesis:_(_m_=_len_q_implies_k1_<_k2_)
assume A34: m = len q ; ::_thesis: k1 < k2
k1 = p . l by A23, A29, A31, Def7;
then k1 in X \ {(k + 1)} by A21, A31, FUNCT_1:def_3;
then A35: k1 <= k by A13, Th1;
q . m = (p ^ <*(k + 1)*>) . ((len p) + (len <*(k + 1)*>)) by A23, A34, Th22
.= (p ^ <*(k + 1)*>) . ((len p) + 1) by Th39
.= k + 1 by Th42 ;
hence k1 < k2 by A30, A35, NAT_1:13; ::_thesis: verum
end;
now__::_thesis:_(_m_<>_len_q_implies_k1_<_k2_)
assume m <> len q ; ::_thesis: k1 < k2
then m < len (p ^ <*(k + 1)*>) by A23, A28, XXREAL_0:1;
then m < (len p) + (len <*(k + 1)*>) by Th22;
then m < (len p) + 1 by Th39;
then A36: m <= len p by NAT_1:13;
then m in Seg (len p) by A32, Th1;
then m in dom p by Def3;
then A37: k2 = p . m by A23, A30, Def7;
k1 = p . l by A23, A29, A31, Def7;
hence k1 < k2 by A22, A26, A27, A36, A37; ::_thesis: verum
end;
hence k1 < k2 by A33; ::_thesis: verum
end;
hence ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) by A25; ::_thesis: verum
end;
hence ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) by A5; ::_thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch_2(A2, A4);
hence ex b1 being FinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
proof
let p, q be FinSequence of NAT ; ::_thesis: ( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) & rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) implies p = q )
assume A38: ( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) & rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) ) ; ::_thesis: p = q
defpred S2[ FinSequence] means for X being set st ex k being Nat st X c= Seg k & $1 is FinSequence of NAT & rng $1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len $1 & k1 = $1 . l & k2 = $1 . m holds
k1 < k2 ) holds
for q being FinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = $1;
A39: S2[ {} ] ;
A40: for p being FinSequence
for x being set st S2[p] holds
S2[p ^ <*x*>]
proof
let p be FinSequence; ::_thesis: for x being set st S2[p] holds
S2[p ^ <*x*>]
let x be set ; ::_thesis: ( S2[p] implies S2[p ^ <*x*>] )
assume A41: S2[p] ; ::_thesis: S2[p ^ <*x*>]
let X be set ; ::_thesis: ( ex k being Nat st X c= Seg k & p ^ <*x*> is FinSequence of NAT & rng (p ^ <*x*>) = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (p ^ <*x*>) & k1 = (p ^ <*x*>) . l & k2 = (p ^ <*x*>) . m holds
k1 < k2 ) implies for q being FinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <*x*> )
given k being Nat such that A42: X c= Seg k ; ::_thesis: ( not p ^ <*x*> is FinSequence of NAT or not rng (p ^ <*x*>) = X or ex l, m, k1, k2 being Nat st
( 1 <= l & l < m & m <= len (p ^ <*x*>) & k1 = (p ^ <*x*>) . l & k2 = (p ^ <*x*>) . m & not k1 < k2 ) or for q being FinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <*x*> )
assume that
A43: p ^ <*x*> is FinSequence of NAT and
A44: rng (p ^ <*x*>) = X and
A45: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (p ^ <*x*>) & k1 = (p ^ <*x*>) . l & k2 = (p ^ <*x*>) . m holds
k1 < k2 ; ::_thesis: for q being FinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <*x*>
let q be FinSequence of NAT ; ::_thesis: ( rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) implies q = p ^ <*x*> )
assume that
A46: rng q = X and
A47: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ; ::_thesis: q = p ^ <*x*>
1 in Seg 1 ;
then A48: 1 in dom <*x*> by Def8;
A49: ex m being Nat st
( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )
proof
<*x*> is FinSequence of NAT by A43, Th36;
then rng <*x*> c= NAT by Def4;
then {x} c= NAT by Th38;
then reconsider m = x as Element of NAT by ZFMISC_1:31;
take m ; ::_thesis: ( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )
thus m = x ; ::_thesis: for l being Nat st l in X & l <> x holds
l < m
thus for l being Nat st l in X & l <> x holds
l < m ::_thesis: verum
proof
let l be Nat; ::_thesis: ( l in X & l <> x implies l < m )
assume that
A50: l in X and
A51: l <> x ; ::_thesis: l < m
consider y being set such that
A52: y in dom (p ^ <*x*>) and
A53: l = (p ^ <*x*>) . y by A44, A50, FUNCT_1:def_3;
A54: y in Seg (len (p ^ <*x*>)) by A52, Def3;
reconsider k = y as Element of NAT by A52;
k <= len (p ^ <*x*>) by A54, Th1;
then k <= (len p) + (len <*x*>) by Th22;
then A55: k <= (len p) + 1 by Th39;
A56: k <> (len p) + 1
proof
assume k = (len p) + 1 ; ::_thesis: contradiction
then (p ^ <*x*>) . k = <*x*> . 1 by A48, Def7
.= x by Def8 ;
hence contradiction by A51, A53; ::_thesis: verum
end;
A57: 1 <= k by A54, Th1;
k < (len p) + 1 by A55, A56, XXREAL_0:1;
then k < (len p) + (len <*x*>) by Th39;
then A58: k < len (p ^ <*x*>) by Th22;
m = (p ^ <*x*>) . ((len p) + 1) by Th42
.= (p ^ <*x*>) . ((len p) + (len <*x*>)) by Th39
.= (p ^ <*x*>) . (len (p ^ <*x*>)) by Th22 ;
hence l < m by A45, A53, A57, A58; ::_thesis: verum
end;
end;
then reconsider m = x as Nat ;
len q <> 0
proof
assume len q = 0 ; ::_thesis: contradiction
then p ^ <*x*> = {} by A44, A46, Lm4, RELAT_1:38;
then 0 = len (p ^ <*x*>)
.= (len p) + (len <*x*>) by Th22
.= 1 + (len p) by Th39 ;
hence contradiction ; ::_thesis: verum
end;
then consider n being Nat such that
A59: len q = n + 1 by NAT_1:6;
deffunc H1( Nat) -> set = q . $1;
ex q9 being FinSequence st
( len q9 = n & ( for m being Nat st m in dom q9 holds
q9 . m = H1(m) ) ) from FINSEQ_1:sch_2();
then consider q9 being FinSequence such that
A60: len q9 = n and
A61: for m being Nat st m in dom q9 holds
q9 . m = q . m ;
now__::_thesis:_for_x_being_set_st_x_in_rng_q9_holds_
x_in_NAT
let x be set ; ::_thesis: ( x in rng q9 implies x in NAT )
assume x in rng q9 ; ::_thesis: x in NAT
then consider y being set such that
A62: y in dom q9 and
A63: x = q9 . y by FUNCT_1:def_3;
A64: y in Seg (len q9) by A62, Def3;
reconsider y = y as Element of NAT by A62;
A65: y <= n by A60, A64, Th1;
A66: n <= n + 1 by NAT_1:11;
A67: 1 <= y by A64, Th1;
y <= n + 1 by A65, A66, XXREAL_0:2;
then y in Seg (n + 1) by A67;
then y in dom q by A59, Def3;
then A68: q . y in rng q by FUNCT_1:def_3;
rng q c= NAT by Def4;
then q . y in NAT by A68;
hence x in NAT by A61, A62, A63; ::_thesis: verum
end;
then rng q9 c= NAT by TARSKI:def_3;
then reconsider f = q9 as FinSequence of NAT by Def4;
A69: dom q = Seg (n + 1) by A59, Def3
.= Seg ((len q9) + (len <*x*>)) by A60, Th39 ;
A70: for m being Nat st m in dom <*x*> holds
q . ((len q9) + m) = <*x*> . m
proof
let m be Nat; ::_thesis: ( m in dom <*x*> implies q . ((len q9) + m) = <*x*> . m )
assume m in dom <*x*> ; ::_thesis: q . ((len q9) + m) = <*x*> . m
then A71: m in {1} by Def8, Th2;
then A72: m = 1 by TARSKI:def_1;
q . ((len q9) + m) = x
proof
assume q . ((len q9) + m) <> x ; ::_thesis: contradiction
then A73: q . (len q) <> x by A59, A60, A71, TARSKI:def_1;
consider d being Nat such that
A74: d = x and
A75: for l being Nat st l in X & l <> x holds
l < d by A49;
x in {x} by TARSKI:def_1;
then x in rng <*x*> by Th38;
then x in (rng p) \/ (rng <*x*>) by XBOOLE_0:def_3;
then x in rng q by A44, A46, Th31;
then consider y being set such that
A76: y in dom q and
A77: x = q . y by FUNCT_1:def_3;
A78: y in Seg (len q) by A76, Def3;
reconsider y = y as Element of NAT by A76;
A79: 1 <= y by A78, Th1;
A80: y <= len q by A78, Th1;
then A81: y < len q by A73, A77, XXREAL_0:1;
1 <= len q by A79, A80, XXREAL_0:2;
then len q in Seg (len q) ;
then A82: len q in dom q by Def3;
A83: q . (len q) in X by A46, A82, FUNCT_1:def_3;
reconsider k = q . (len q) as Nat ;
k < d by A73, A75, A83;
hence contradiction by A47, A74, A77, A79, A81; ::_thesis: verum
end;
hence q . ((len q9) + m) = <*x*> . m by A72, Th40; ::_thesis: verum
end;
then A84: q9 ^ <*x*> = q by A61, A69, Def7;
A85: ex m being Nat st X \ {x} c= Seg m by A42, XBOOLE_1:1;
A86: not x in rng p
proof
assume x in rng p ; ::_thesis: contradiction
then consider y being set such that
A87: y in dom p and
A88: x = p . y by FUNCT_1:def_3;
A89: y in Seg (len p) by A87, Def3;
reconsider y = y as Element of NAT by A87;
A90: y <= len p by A89, Th1;
A91: (len p) + 1 = (len p) + (len <*x*>) by Th39
.= len (p ^ <*x*>) by Th22 ;
A92: 1 <= y by A89, Th1;
A93: y < (len p) + 1 by A90, NAT_1:13;
A94: m = (p ^ <*x*>) . y by A87, A88, Def7;
m = (p ^ <*x*>) . ((len p) + 1) by Th42;
hence contradiction by A45, A91, A92, A93, A94; ::_thesis: verum
end;
A95: X = (rng p) \/ (rng <*x*>) by A44, Th31
.= (rng p) \/ {x} by Th39 ;
A96: for z being set holds
( z in ((rng p) \/ {x}) \ {x} iff z in rng p )
proof
let z be set ; ::_thesis: ( z in ((rng p) \/ {x}) \ {x} iff z in rng p )
thus ( z in ((rng p) \/ {x}) \ {x} implies z in rng p ) ::_thesis: ( z in rng p implies z in ((rng p) \/ {x}) \ {x} )
proof
assume A97: z in ((rng p) \/ {x}) \ {x} ; ::_thesis: z in rng p
then not z in {x} by XBOOLE_0:def_5;
hence z in rng p by A97, XBOOLE_0:def_3; ::_thesis: verum
end;
assume z in rng p ; ::_thesis: z in ((rng p) \/ {x}) \ {x}
then ( not z in {x} & z in (rng p) \/ {x} ) by A86, TARSKI:def_1, XBOOLE_0:def_3;
hence z in ((rng p) \/ {x}) \ {x} by XBOOLE_0:def_5; ::_thesis: verum
end;
A98: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2
proof
let l, m, k1, k2 be Nat; ::_thesis: ( 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m implies k1 < k2 )
assume that
A99: 1 <= l and
A100: l < m and
A101: m <= len p and
A102: k1 = p . l and
A103: k2 = p . m ; ::_thesis: k1 < k2
l <= len p by A100, A101, XXREAL_0:2;
then l in Seg (len p) by A99, Th1;
then l in dom p by Def3;
then A104: k1 = (p ^ <*x*>) . l by A102, Def7;
1 <= m by A99, A100, XXREAL_0:2;
then m in Seg (len p) by A101, Th1;
then m in dom p by Def3;
then A105: k2 = (p ^ <*x*>) . m by A103, Def7;
len p <= (len p) + 1 by NAT_1:11;
then m <= (len p) + 1 by A101, XXREAL_0:2;
then m <= (len p) + (len <*x*>) by Th39;
then m <= len (p ^ <*x*>) by Th22;
hence k1 < k2 by A45, A99, A100, A104, A105; ::_thesis: verum
end;
A106: p is FinSequence of NAT by A43, Th36;
A107: rng p = X \ {x} by A95, A96, TARSKI:1;
A108: not x in rng f
proof
assume x in rng f ; ::_thesis: contradiction
then consider y being set such that
A109: y in dom f and
A110: x = f . y by FUNCT_1:def_3;
A111: y in Seg (len f) by A109, Def3;
reconsider y = y as Element of NAT by A109;
A112: y <= len f by A111, Th1;
A113: (len f) + 1 = (len f) + (len <*x*>) by Th39
.= len (f ^ <*x*>) by Th22 ;
A114: 1 <= y by A111, Th1;
A115: y < (len f) + 1 by A112, NAT_1:13;
A116: m = q . y by A61, A109, A110;
m = q . ((len f) + 1) by A84, Th42;
hence contradiction by A47, A84, A113, A114, A115, A116; ::_thesis: verum
end;
A117: X = (rng f) \/ (rng <*x*>) by A46, A84, Th31
.= (rng f) \/ {x} by Th39 ;
A118: for z being set holds
( z in ((rng f) \/ {x}) \ {x} iff z in rng f )
proof
let z be set ; ::_thesis: ( z in ((rng f) \/ {x}) \ {x} iff z in rng f )
thus ( z in ((rng f) \/ {x}) \ {x} implies z in rng f ) ::_thesis: ( z in rng f implies z in ((rng f) \/ {x}) \ {x} )
proof
assume A119: z in ((rng f) \/ {x}) \ {x} ; ::_thesis: z in rng f
then not z in {x} by XBOOLE_0:def_5;
hence z in rng f by A119, XBOOLE_0:def_3; ::_thesis: verum
end;
assume z in rng f ; ::_thesis: z in ((rng f) \/ {x}) \ {x}
then ( not z in {x} & z in (rng f) \/ {x} ) by A108, TARSKI:def_1, XBOOLE_0:def_3;
hence z in ((rng f) \/ {x}) \ {x} by XBOOLE_0:def_5; ::_thesis: verum
end;
A120: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len f & k1 = f . l & k2 = f . m holds
k1 < k2
proof
let l, m, k1, k2 be Nat; ::_thesis: ( 1 <= l & l < m & m <= len f & k1 = f . l & k2 = f . m implies k1 < k2 )
assume that
A121: 1 <= l and
A122: l < m and
A123: m <= len f and
A124: k1 = f . l and
A125: k2 = f . m ; ::_thesis: k1 < k2
A126: m <= len q by A59, A60, A123, NAT_1:13;
l <= n by A60, A122, A123, XXREAL_0:2;
then A127: l in Seg n by A121, Th1;
1 <= m by A121, A122, XXREAL_0:2;
then A128: m in Seg n by A60, A123, Th1;
A129: l in dom q9 by A60, A127, Def3;
A130: m in dom q9 by A60, A128, Def3;
A131: k1 = q . l by A61, A124, A129;
k2 = q . m by A61, A125, A130;
hence k1 < k2 by A47, A121, A122, A126, A131; ::_thesis: verum
end;
rng f = X \ {x} by A117, A118, TARSKI:1;
then q9 = p by A41, A85, A98, A106, A107, A120;
hence q = p ^ <*x*> by A61, A69, A70, Def7; ::_thesis: verum
end;
for p being FinSequence holds S2[p] from FINSEQ_1:sch_3(A39, A40);
hence p = q by A1, A38; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines Sgm FINSEQ_1:def_13_:_
for X being set st ex k being Nat st X c= Seg k holds
for b2 being FinSequence of NAT holds
( b2 = Sgm X iff ( rng b2 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) ) );
theorem Th50: :: FINSEQ_1:50
for p9 being FinSubsequence holds rng (Sgm (dom p9)) = dom p9
proof
let p9 be FinSubsequence; ::_thesis: rng (Sgm (dom p9)) = dom p9
ex k being Nat st dom p9 c= Seg k by Def12;
hence rng (Sgm (dom p9)) = dom p9 by Def13; ::_thesis: verum
end;
definition
let p9 be FinSubsequence;
func Seq p9 -> Function equals :: FINSEQ_1:def 14
p9 * (Sgm (dom p9));
coherence
p9 * (Sgm (dom p9)) is Function ;
end;
:: deftheorem defines Seq FINSEQ_1:def_14_:_
for p9 being FinSubsequence holds Seq p9 = p9 * (Sgm (dom p9));
registration
let p9 be FinSubsequence;
cluster Seq p9 -> FinSequence-like ;
coherence
Seq p9 is FinSequence-like
proof
rng (Sgm (dom p9)) = dom p9 by Th50;
then dom (p9 * (Sgm (dom p9))) = dom (Sgm (dom p9)) by RELAT_1:27
.= Seg (len (Sgm (dom p9))) by Def3 ;
hence Seq p9 is FinSequence-like by Def2; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:51
for X being set st ex k being Nat st X c= Seg k holds
( Sgm X = {} iff X = {} )
proof
let X be set ; ::_thesis: ( ex k being Nat st X c= Seg k implies ( Sgm X = {} iff X = {} ) )
given k being Nat such that A1: X c= Seg k ; ::_thesis: ( Sgm X = {} iff X = {} )
thus ( Sgm X = {} implies X = {} ) ::_thesis: ( X = {} implies Sgm X = {} )
proof
assume Sgm X = {} ; ::_thesis: X = {}
hence X = rng {} by A1, Def13
.= {} ;
::_thesis: verum
end;
assume X = {} ; ::_thesis: Sgm X = {}
then rng (Sgm X) = {} by A1, Def13;
hence Sgm X = {} ; ::_thesis: verum
end;
begin
theorem :: FINSEQ_1:52
for D being set holds
( D is finite iff ex p being FinSequence st D = rng p )
proof
let D be set ; ::_thesis: ( D is finite iff ex p being FinSequence st D = rng p )
thus ( D is finite implies ex p being FinSequence st D = rng p ) ::_thesis: ( ex p being FinSequence st D = rng p implies D is finite )
proof
given g being Function such that A1: rng g = D and
A2: dom g in omega ; :: according to FINSET_1:def_1 ::_thesis: ex p being FinSequence st D = rng p
reconsider n = dom g as Element of NAT by A2;
defpred S2[ set , set ] means S1[$2,$1];
A3: for x being set st x in Seg n holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in Seg n implies ex y being set st S2[x,y] )
assume A4: x in Seg n ; ::_thesis: ex y being set st S2[x,y]
then reconsider x = x as Element of NAT ;
x >= 1 by A4, Th1;
then ex k being Nat st x = 1 + k by NAT_1:10;
hence ex y being set st S2[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A5: dom f = Seg n and
A6: for x being set st x in Seg n holds
S2[x,f . x] from CLASSES1:sch_1(A3);
A7: rng f = dom g
proof
A8: n = { k where k is Element of NAT : k < n } by AXIOMS:4;
thus rng f c= dom g :: according to XBOOLE_0:def_10 ::_thesis: dom g c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in dom g )
assume x in rng f ; ::_thesis: x in dom g
then consider y being set such that
A9: y in dom f and
A10: x = f . y by FUNCT_1:def_3;
consider k being Nat such that
A11: x = k and
A12: y = k + 1 by A5, A6, A9, A10;
k + 1 <= n by A5, A9, A12, Th1;
then ( k in NAT & k < n ) by NAT_1:13, ORDINAL1:def_12;
hence x in dom g by A8, A11; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in rng f )
assume x in dom g ; ::_thesis: x in rng f
then consider k being Element of NAT such that
A13: x = k and
A14: k < n by A8;
( 1 <= k + 1 & k + 1 <= n ) by A14, NAT_1:11, NAT_1:13;
then A15: k + 1 in Seg n ;
then ex k1 being Nat st
( f . (k + 1) = k1 & k + 1 = k1 + 1 ) by A6;
hence x in rng f by A5, A13, A15, FUNCT_1:def_3; ::_thesis: verum
end;
then dom (g * f) = Seg n by A5, RELAT_1:27;
then reconsider p = g * f as FinSequence by Def2;
take p ; ::_thesis: D = rng p
thus D = rng p by A1, A7, RELAT_1:28; ::_thesis: verum
end;
given p being FinSequence such that A16: D = rng p ; ::_thesis: D is finite
consider n being Nat such that
A17: dom p = Seg n by Def2;
A18: n = { k where k is Element of NAT : k < n } by AXIOMS:4;
A19: for x being set st x in n holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in n implies ex y being set st S1[x,y] )
assume x in n ; ::_thesis: ex y being set st S1[x,y]
then ex k being Element of NAT st
( x = k & k < n ) by A18;
then reconsider k = x as Nat ;
take k + 1 ; ::_thesis: S1[x,k + 1]
thus S1[x,k + 1] ; ::_thesis: verum
end;
consider f being Function such that
A20: dom f = n and
A21: for x being set st x in n holds
S1[x,f . x] from CLASSES1:sch_1(A19);
take p * f ; :: according to FINSET_1:def_1 ::_thesis: ( rng (p * f) = D & dom (p * f) in omega )
A22: rng f = dom p
proof
thus rng f c= dom p :: according to XBOOLE_0:def_10 ::_thesis: dom p c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in dom p )
assume x in rng f ; ::_thesis: x in dom p
then consider y being set such that
A23: y in dom f and
A24: x = f . y by FUNCT_1:def_3;
consider k being Nat such that
A25: y = k and
A26: x = k + 1 by A20, A21, A23, A24;
ex m being Element of NAT st
( k = m & m < n ) by A18, A20, A23, A25;
then ( 1 <= k + 1 & k + 1 <= n ) by NAT_1:11, NAT_1:13;
hence x in dom p by A17, A26; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom p or x in rng f )
assume A27: x in dom p ; ::_thesis: x in rng f
then reconsider x = x as Element of NAT ;
1 <= x by A17, A27, Th1;
then consider m being Nat such that
A28: x = 1 + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
x <= n by A17, A27, Th1;
then m < n by A28, NAT_1:13;
then A29: m in n by A18;
then ex k being Nat st
( m = k & f . m = k + 1 ) by A21;
hence x in rng f by A20, A28, A29, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng (p * f) = D by A16, RELAT_1:28; ::_thesis: dom (p * f) in omega
dom (p * f) = dom f by A22, RELAT_1:27;
hence dom (p * f) in omega by A20, ORDINAL1:def_12; ::_thesis: verum
end;
begin
theorem :: FINSEQ_1:53
for n, m being Nat st Seg n, Seg m are_equipotent holds
n = m
proof
let n, m be Nat; ::_thesis: ( Seg n, Seg m are_equipotent implies n = m )
defpred S2[ Nat] means ex n being Nat st
( Seg n, Seg $1 are_equipotent & n <> $1 );
assume ( Seg n, Seg m are_equipotent & n <> m ) ; ::_thesis: contradiction
then A1: ex m being Nat st S2[m] ;
consider m being Nat such that
A2: S2[m] and
A3: for k being Nat st S2[k] holds
m <= k from NAT_1:sch_5(A1);
consider n being Nat such that
A4: Seg n, Seg m are_equipotent and
A5: n <> m by A2;
A6: ex f being Function st
( f is one-to-one & dom f = Seg n & rng f = Seg m ) by A4, WELLORD2:def_4;
A7: now__::_thesis:_not_m_=_0
assume m = 0 ; ::_thesis: contradiction
then Seg m = {} ;
then Seg m = Seg n by A6, RELAT_1:42;
hence contradiction by A5, Th6; ::_thesis: verum
end;
then consider m1 being Nat such that
A8: m = m1 + 1 by NAT_1:6;
A9: now__::_thesis:_not_n_=_0
assume n = 0 ; ::_thesis: contradiction
then Seg n = {} ;
then Seg m = Seg n by A6, RELAT_1:42;
hence contradiction by A5, Th6; ::_thesis: verum
end;
then consider n1 being Nat such that
A10: n = n1 + 1 by NAT_1:6;
reconsider m1 = m1, n1 = n1 as Element of NAT by ORDINAL1:def_12;
A11: n in Seg n by A9, Th3;
A12: m in Seg m by A7, Th3;
A13: not n1 + 1 <= n1 by NAT_1:13;
A14: not m1 + 1 <= m1 by NAT_1:13;
A15: not n in Seg n1 by A10, A13, Th1;
A16: not m in Seg m1 by A8, A14, Th1;
A17: (Seg n1) /\ {n} c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Seg n1) /\ {n} or x in {} )
assume x in (Seg n1) /\ {n} ; ::_thesis: x in {}
then ( x in Seg n1 & x in {n} ) by XBOOLE_0:def_4;
hence x in {} by A15, TARSKI:def_1; ::_thesis: verum
end;
A18: (Seg m1) /\ {m} c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Seg m1) /\ {m} or x in {} )
assume x in (Seg m1) /\ {m} ; ::_thesis: x in {}
then ( x in Seg m1 & x in {m} ) by XBOOLE_0:def_4;
hence x in {} by A16, TARSKI:def_1; ::_thesis: verum
end;
A19: Seg n = (Seg n1) \/ {n} by A10, Th9;
A20: Seg m = (Seg m1) \/ {m} by A8, Th9;
A21: (Seg n1) /\ {n} = {} by A17;
A22: (Seg m1) /\ {m} = {} by A18;
A23: ( (Seg n1) \ {n} = ((Seg n1) \/ {n}) \ {n} & Seg n1 misses {n} ) by A21, XBOOLE_0:def_7, XBOOLE_1:40;
A24: ( (Seg m1) \ {m} = ((Seg m1) \/ {m}) \ {m} & Seg m1 misses {m} ) by A22, XBOOLE_0:def_7, XBOOLE_1:40;
A25: (Seg n) \ {n} = Seg n1 by A19, A23, XBOOLE_1:83;
(Seg m) \ {m} = Seg m1 by A20, A24, XBOOLE_1:83;
hence contradiction by A3, A4, A5, A8, A10, A11, A12, A14, A25, CARD_1:34; ::_thesis: verum
end;
theorem :: FINSEQ_1:54
for n being Nat holds Seg n,n are_equipotent by Lm1;
theorem :: FINSEQ_1:55
for n being Nat holds card (Seg n) = card n by Lm2;
theorem :: FINSEQ_1:56
for X being set st X is finite holds
ex n being Nat st X, Seg n are_equipotent
proof
let X be set ; ::_thesis: ( X is finite implies ex n being Nat st X, Seg n are_equipotent )
assume X is finite ; ::_thesis: ex n being Nat st X, Seg n are_equipotent
then consider n being Nat such that
A1: X,n are_equipotent by CARD_1:43;
take n ; ::_thesis: X, Seg n are_equipotent
n, Seg n are_equipotent by Lm1;
hence X, Seg n are_equipotent by A1, WELLORD2:15; ::_thesis: verum
end;
theorem :: FINSEQ_1:57
for n being Nat holds card (Seg n) = n
proof
let n be Nat; ::_thesis: card (Seg n) = n
Seg n,n are_equipotent by Lm1;
hence card (Seg n) = n by CARD_1:def_2; ::_thesis: verum
end;
begin
registration
let x be set ;
cluster<*x*> -> non empty ;
coherence
not <*x*> is empty ;
end;
registration
cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like for set ;
existence
not for b1 being FinSequence holds b1 is empty
proof
take <*0*> ; ::_thesis: not <*0*> is empty
thus not <*0*> is empty ; ::_thesis: verum
end;
end;
registration
let f1 be FinSequence;
let f2 be non empty FinSequence;
clusterf1 ^ f2 -> non empty ;
coherence
not f1 ^ f2 is empty by Th35;
clusterf2 ^ f1 -> non empty ;
coherence
not f2 ^ f1 is empty by Th35;
end;
registration
let x, y be set ;
cluster<*x,y*> -> non empty ;
coherence
not <*x,y*> is empty ;
let z be set ;
cluster<*x,y,z*> -> non empty ;
coherence
not <*x,y,z*> is empty ;
end;
scheme :: FINSEQ_1:sch 5
SeqDEx{ F1() -> non empty set , F2() -> Nat, P1[ set , set ] } :
ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p . k] ) )
provided
A1: for k being Nat st k in Seg F2() holds
ex x being Element of F1() st P1[k,x]
proof
A2: for y being set st y in Seg F2() holds
ex x being set st
( x in F1() & P1[y,x] )
proof
let y be set ; ::_thesis: ( y in Seg F2() implies ex x being set st
( x in F1() & P1[y,x] ) )
assume A3: y in Seg F2() ; ::_thesis: ex x being set st
( x in F1() & P1[y,x] )
then reconsider k = y as Element of NAT ;
consider x being Element of F1() such that
A4: P1[k,x] by A1, A3;
take x ; ::_thesis: ( x in F1() & P1[y,x] )
thus ( x in F1() & P1[y,x] ) by A4; ::_thesis: verum
end;
consider f being Function such that
A5: dom f = Seg F2() and
A6: rng f c= F1() and
A7: for y being set st y in Seg F2() holds
P1[y,f . y] from FUNCT_1:sch_5(A2);
reconsider f = f as FinSequence by A5, Def2;
reconsider p = f as FinSequence of F1() by A6, Def4;
take p ; ::_thesis: ( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p . k] ) )
thus ( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p . k] ) ) by A5, A7; ::_thesis: verum
end;
definition
let m be Nat;
let p be FinSequence;
funcp | m -> FinSequence equals :: FINSEQ_1:def 15
p | (Seg m);
coherence
p | (Seg m) is FinSequence by Th15;
end;
:: deftheorem defines | FINSEQ_1:def_15_:_
for m being Nat
for p being FinSequence holds p | m = p | (Seg m);
definition
let D be set ;
let m be Nat;
let p be FinSequence of D;
:: original: |
redefine funcp | m -> FinSequence of D;
coherence
p | m is FinSequence of D by Th18;
end;
registration
let f be FinSequence;
clusterf | 0 -> empty ;
coherence
f | 0 is empty ;
end;
theorem :: FINSEQ_1:58
for i being Nat
for q being FinSequence st len q <= i holds
q | i = q
proof
let i be Nat; ::_thesis: for q being FinSequence st len q <= i holds
q | i = q
let q be FinSequence; ::_thesis: ( len q <= i implies q | i = q )
assume len q <= i ; ::_thesis: q | i = q
then Seg (len q) c= Seg i by Th5;
then dom q c= Seg i by Def3;
hence q | i = q by RELAT_1:68; ::_thesis: verum
end;
theorem :: FINSEQ_1:59
for i being Nat
for q being FinSequence st i <= len q holds
len (q | i) = i
proof
let i be Nat; ::_thesis: for q being FinSequence st i <= len q holds
len (q | i) = i
let q be FinSequence; ::_thesis: ( i <= len q implies len (q | i) = i )
assume i <= len q ; ::_thesis: len (q | i) = i
then Seg i c= Seg (len q) by Th5;
then Seg i c= dom q by Def3;
then ( i in NAT & Seg i = dom (q | i) ) by ORDINAL1:def_12, RELAT_1:62;
hence len (q | i) = i by Def3; ::_thesis: verum
end;
theorem :: FINSEQ_1:60
for i, n, m being Nat st i in Seg n holds
i + m in Seg (n + m)
proof
let i, n, m be Nat; ::_thesis: ( i in Seg n implies i + m in Seg (n + m) )
assume A1: i in Seg n ; ::_thesis: i + m in Seg (n + m)
then A2: 1 <= i by Th1;
A3: i <= n by A1, Th1;
i <= i + m by NAT_1:11;
then A4: 1 <= i + m by A2, XXREAL_0:2;
i + m <= n + m by A3, XREAL_1:7;
hence i + m in Seg (n + m) by A4, Th1; ::_thesis: verum
end;
theorem :: FINSEQ_1:61
for i, n, m being Nat st i > 0 & i + m in Seg (n + m) holds
( i in Seg n & i in Seg (n + m) )
proof
let i, n, m be Nat; ::_thesis: ( i > 0 & i + m in Seg (n + m) implies ( i in Seg n & i in Seg (n + m) ) )
assume that
A1: i > 0 and
A2: i + m in Seg (n + m) ; ::_thesis: ( i in Seg n & i in Seg (n + m) )
1 = 0 + 1 ;
then A3: 1 <= i by A1, NAT_1:13;
A4: i + m <= n + m by A2, Th1;
then i <= n by XREAL_1:6;
hence i in Seg n by A3, Th1; ::_thesis: i in Seg (n + m)
i <= i + m by NAT_1:11;
then i <= n + m by A4, XXREAL_0:2;
hence i in Seg (n + m) by A3, Th1; ::_thesis: verum
end;
definition
let R be Relation;
funcR [*] -> Relation means :: FINSEQ_1:def 16
for x, y being set holds
( [x,y] in it iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) )
proof
defpred S2[ set , set ] means ex p being FinSequence st
( len p >= 1 & p . 1 = $1 & p . (len p) = $2 & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) );
thus ex S being Relation st
for x, y being set holds
( [x,y] in S iff ( x in field R & y in field R & S2[x,y] ) ) from RELAT_1:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) holds
b1 = b2
proof
let R1, R2 be Relation; ::_thesis: ( ( for x, y being set holds
( [x,y] in R1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) & ( for x, y being set holds
( [x,y] in R2 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) implies R1 = R2 )
assume that
A1: for x, y being set holds
( [x,y] in R1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) and
A2: for x, y being set holds
( [x,y] in R2 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ; ::_thesis: R1 = R2
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
thus ( [x,y] in R1 implies [x,y] in R2 ) ::_thesis: ( not [x,y] in R2 or [x,y] in R1 )
proof
assume A3: [x,y] in R1 ; ::_thesis: [x,y] in R2
then A4: ( x in field R & y in field R ) by A1;
ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) by A1, A3;
hence [x,y] in R2 by A2, A4; ::_thesis: verum
end;
assume A5: [x,y] in R2 ; ::_thesis: [x,y] in R1
then A6: ( x in field R & y in field R ) by A2;
ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) by A2, A5;
hence [x,y] in R1 by A1, A6; ::_thesis: verum
end;
end;
:: deftheorem defines [*] FINSEQ_1:def_16_:_
for R, b2 being Relation holds
( b2 = R [*] iff for x, y being set holds
( [x,y] in b2 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) );
theorem :: FINSEQ_1:62
for D1, D2 being set st D1 c= D2 holds
D1 * c= D2 *
proof
let D1, D2 be set ; ::_thesis: ( D1 c= D2 implies D1 * c= D2 * )
assume A1: D1 c= D2 ; ::_thesis: D1 * c= D2 *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 * or x in D2 * )
assume x in D1 * ; ::_thesis: x in D2 *
then reconsider p = x as FinSequence of D1 by Def11;
rng p c= D1 by Def4;
then rng p c= D2 by A1, XBOOLE_1:1;
then x is FinSequence of D2 by Def4;
hence x in D2 * by Def11; ::_thesis: verum
end;
registration
let D be set ;
clusterD * -> functional ;
coherence
D * is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in D * or x is set )
thus ( not x in D * or x is set ) by Def11; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:63
for p, q being FinSequence st p c= q holds
len p <= len q
proof
let p, q be FinSequence; ::_thesis: ( p c= q implies len p <= len q )
assume p c= q ; ::_thesis: len p <= len q
then card p c= card q by CARD_1:11;
hence len p <= len q by NAT_1:39; ::_thesis: verum
end;
theorem :: FINSEQ_1:64
for p, q being FinSequence
for i being Nat st 1 <= i & i <= len p holds
(p ^ q) . i = p . i
proof
let p, q be FinSequence; ::_thesis: for i being Nat st 1 <= i & i <= len p holds
(p ^ q) . i = p . i
let i be Nat; ::_thesis: ( 1 <= i & i <= len p implies (p ^ q) . i = p . i )
assume A1: ( 1 <= i & i <= len p ) ; ::_thesis: (p ^ q) . i = p . i
( i in NAT & Seg (len p) = dom p ) by Def3, ORDINAL1:def_12;
then i in dom p by A1;
hence (p ^ q) . i = p . i by Def7; ::_thesis: verum
end;
theorem :: FINSEQ_1:65
for p, q being FinSequence
for i being Nat st 1 <= i & i <= len q holds
(p ^ q) . ((len p) + i) = q . i
proof
let p, q be FinSequence; ::_thesis: for i being Nat st 1 <= i & i <= len q holds
(p ^ q) . ((len p) + i) = q . i
let i be Nat; ::_thesis: ( 1 <= i & i <= len q implies (p ^ q) . ((len p) + i) = q . i )
assume ( 1 <= i & i <= len q ) ; ::_thesis: (p ^ q) . ((len p) + i) = q . i
then ( (len p) + 1 <= (len p) + i & (len p) + i <= (len p) + (len q) ) by XREAL_1:6;
hence (p ^ q) . ((len p) + i) = q . (((len p) + i) - (len p)) by Th23
.= q . i ;
::_thesis: verum
end;
scheme :: FINSEQ_1:sch 6
FinSegRng{ F1() -> Nat, F2() -> Nat, F3( set ) -> set , P1[ set ] } :
{ F3(i) where i is Element of NAT : ( F1() <= i & i <= F2() & P1[i] ) } is finite
proof
set F = { F3(i) where i is Element of NAT : ( F1() <= i & i <= F2() & P1[i] ) } ;
deffunc H1( Nat) -> set = F3(($1 - 1));
consider f being FinSequence such that
A1: len f = F2() + 1 and
A2: for k being Nat st k in dom f holds
f . k = H1(k) from FINSEQ_1:sch_2();
{ F3(i) where i is Element of NAT : ( F1() <= i & i <= F2() & P1[i] ) } c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(i) where i is Element of NAT : ( F1() <= i & i <= F2() & P1[i] ) } or x in rng f )
assume x in { F3(i) where i is Element of NAT : ( F1() <= i & i <= F2() & P1[i] ) } ; ::_thesis: x in rng f
then consider j being Element of NAT such that
A3: x = F3(j) and
F1() <= j and
A4: j <= F2() and
P1[j] ;
( 1 <= j + 1 & j + 1 <= F2() + 1 ) by A4, NAT_1:11, XREAL_1:6;
then j + 1 in Seg (F2() + 1) ;
then A5: j + 1 in dom f by A1, Def3;
then f . (j + 1) = F3(((j + 1) - 1)) by A2
.= F3(j) ;
hence x in rng f by A3, A5, FUNCT_1:def_3; ::_thesis: verum
end;
hence { F3(i) where i is Element of NAT : ( F1() <= i & i <= F2() & P1[i] ) } is finite ; ::_thesis: verum
end;
Lm6: ( 1 in Seg 3 & 2 in Seg 3 )
;
Lm7: 3 in Seg 3
;
Lm8: ( 1 in Seg 4 & 2 in Seg 4 )
;
Lm9: ( 3 in Seg 4 & 4 in Seg 4 )
;
Lm10: ( 1 in Seg 5 & 2 in Seg 5 )
;
Lm11: ( 3 in Seg 5 & 4 in Seg 5 )
;
Lm12: 5 in Seg 5
;
Lm13: ( 1 in Seg 6 & 2 in Seg 6 )
;
Lm14: ( 3 in Seg 6 & 4 in Seg 6 )
;
Lm15: ( 5 in Seg 6 & 6 in Seg 6 )
;
Lm16: ( 1 in Seg 7 & 2 in Seg 7 )
;
Lm17: ( 3 in Seg 7 & 4 in Seg 7 )
;
Lm18: ( 5 in Seg 7 & 6 in Seg 7 )
;
Lm19: 7 in Seg 7
;
Lm20: ( 1 in Seg 8 & 2 in Seg 8 )
;
Lm21: ( 3 in Seg 8 & 4 in Seg 8 )
;
Lm22: ( 5 in Seg 8 & 6 in Seg 8 )
;
Lm23: ( 7 in Seg 8 & 8 in Seg 8 )
;
theorem Th66: :: FINSEQ_1:66
for x1, x2, x3, x4 being set
for p being FinSequence st p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> holds
( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
proof
let x1, x2, x3, x4 be set ; ::_thesis: for p being FinSequence st p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> holds
( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
let p be FinSequence; ::_thesis: ( p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> implies ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
assume A1: p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ; ::_thesis: ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
set p13 = (<*x1*> ^ <*x2*>) ^ <*x3*>;
A2: (<*x1*> ^ <*x2*>) ^ <*x3*> = <*x1,x2,x3*> ;
then A3: len ((<*x1*> ^ <*x2*>) ^ <*x3*>) = 3 by Th45;
A4: ( ((<*x1*> ^ <*x2*>) ^ <*x3*>) . 1 = x1 & ((<*x1*> ^ <*x2*>) ^ <*x3*>) . 2 = x2 ) by A2, Th45;
A5: ((<*x1*> ^ <*x2*>) ^ <*x3*>) . 3 = x3 by A2, Th45;
thus len p = (len ((<*x1*> ^ <*x2*>) ^ <*x3*>)) + (len <*x4*>) by A1, Th22
.= 3 + 1 by A3, Th40
.= 4 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
dom ((<*x1*> ^ <*x2*>) ^ <*x3*>) = Seg 3 by A3, Def3;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 ) by A1, A4, A5, Def7, Lm6, Lm7; ::_thesis: p . 4 = x4
thus p . 4 = p . ((len ((<*x1*> ^ <*x2*>) ^ <*x3*>)) + 1) by A3
.= x4 by A1, Th42 ; ::_thesis: verum
end;
theorem Th67: :: FINSEQ_1:67
for x1, x2, x3, x4, x5 being set
for p being FinSequence st p = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> holds
( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: for p being FinSequence st p = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> holds
( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
let p be FinSequence; ::_thesis: ( p = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> implies ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )
assume A1: p = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> ; ::_thesis: ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
set p14 = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>;
A2: len (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) = 4 by Th66;
A3: ( (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 1 = x1 & (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 2 = x2 ) by Th66;
A4: ( (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 3 = x3 & (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 4 = x4 ) by Th66;
thus len p = (len (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>)) + (len <*x5*>) by A1, Th22
.= 4 + 1 by A2, Th40
.= 5 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
dom (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) = Seg 4 by A2, Def3;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) by A1, A3, A4, Def7, Lm8, Lm9; ::_thesis: p . 5 = x5
thus p . 5 = p . ((len (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>)) + 1) by A2
.= x5 by A1, Th42 ; ::_thesis: verum
end;
theorem Th68: :: FINSEQ_1:68
for x1, x2, x3, x4, x5, x6 being set
for p being FinSequence st p = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*> holds
( len p = 6 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 )
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: for p being FinSequence st p = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*> holds
( len p = 6 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 )
let p be FinSequence; ::_thesis: ( p = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*> implies ( len p = 6 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 ) )
assume A1: p = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*> ; ::_thesis: ( len p = 6 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 )
set p15 = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>;
A2: len ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) = 5 by Th67;
A3: ( ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) . 1 = x1 & ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) . 2 = x2 ) by Th67;
A4: ( ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) . 3 = x3 & ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) . 4 = x4 ) by Th67;
A5: ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) . 5 = x5 by Th67;
thus len p = (len ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>)) + (len <*x6*>) by A1, Th22
.= 5 + 1 by A2, Th40
.= 6 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 )
dom ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) = Seg 5 by A2, Def3;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) by A1, A3, A4, A5, Def7, Lm10, Lm11, Lm12; ::_thesis: p . 6 = x6
thus p . 6 = p . ((len ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>)) + 1) by A2
.= x6 by A1, Th42 ; ::_thesis: verum
end;
theorem Th69: :: FINSEQ_1:69
for x1, x2, x3, x4, x5, x6, x7 being set
for p being FinSequence st p = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*> holds
( len p = 7 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 )
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: for p being FinSequence st p = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*> holds
( len p = 7 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 )
let p be FinSequence; ::_thesis: ( p = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*> implies ( len p = 7 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 ) )
assume A1: p = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*> ; ::_thesis: ( len p = 7 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 )
set p16 = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>;
A2: len (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) = 6 by Th68;
A3: ( (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) . 1 = x1 & (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) . 2 = x2 ) by Th68;
A4: ( (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) . 3 = x3 & (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) . 4 = x4 ) by Th68;
A5: ( (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) . 5 = x5 & (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) . 6 = x6 ) by Th68;
thus len p = (len (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>)) + (len <*x7*>) by A1, Th22
.= 6 + 1 by A2, Th40
.= 7 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 )
dom (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) = Seg 6 by A2, Def3;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 ) by A1, A3, A4, A5, Def7, Lm13, Lm14, Lm15; ::_thesis: p . 7 = x7
thus p . 7 = p . ((len (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>)) + 1) by A2
.= x7 by A1, Th42 ; ::_thesis: verum
end;
theorem Th70: :: FINSEQ_1:70
for x1, x2, x3, x4, x5, x6, x7, x8 being set
for p being FinSequence st p = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*> holds
( len p = 8 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 )
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: for p being FinSequence st p = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*> holds
( len p = 8 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 )
let p be FinSequence; ::_thesis: ( p = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*> implies ( len p = 8 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 ) )
assume A1: p = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*> ; ::_thesis: ( len p = 8 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 )
set p17 = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>;
A2: len ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) = 7 by Th69;
A3: ( ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) . 1 = x1 & ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) . 2 = x2 ) by Th69;
A4: ( ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) . 3 = x3 & ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) . 4 = x4 ) by Th69;
A5: ( ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) . 5 = x5 & ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) . 6 = x6 ) by Th69;
A6: ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) . 7 = x7 by Th69;
thus len p = (len ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>)) + (len <*x8*>) by A1, Th22
.= 7 + 1 by A2, Th40
.= 8 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 )
dom ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) = Seg 7 by A2, Def3;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 ) by A1, A3, A4, A5, A6, Def7, Lm16, Lm17, Lm18, Lm19; ::_thesis: p . 8 = x8
thus p . 8 = p . ((len ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>)) + 1) by A2
.= x8 by A1, Th42 ; ::_thesis: verum
end;
theorem :: FINSEQ_1:71
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set
for p being FinSequence st p = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*> holds
( len p = 9 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 )
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: for p being FinSequence st p = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*> holds
( len p = 9 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 )
let p be FinSequence; ::_thesis: ( p = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*> implies ( len p = 9 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 ) )
assume A1: p = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*> ; ::_thesis: ( len p = 9 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 )
set p17 = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>;
A2: len (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) = 8 by Th70;
A3: ( (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 1 = x1 & (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 2 = x2 ) by Th70;
A4: ( (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 3 = x3 & (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 4 = x4 ) by Th70;
A5: ( (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 5 = x5 & (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 6 = x6 ) by Th70;
A6: ( (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 7 = x7 & (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) . 8 = x8 ) by Th70;
thus len p = (len (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>)) + (len <*x9*>) by A1, Th22
.= 8 + 1 by A2, Th40
.= 9 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 )
dom (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) = Seg 8 by A2, Def3;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 ) by A1, A3, A4, A5, A6, Def7, Lm20, Lm21, Lm22, Lm23; ::_thesis: p . 9 = x9
thus p . 9 = p . ((len (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>)) + 1) by A2
.= x9 by A1, Th42 ; ::_thesis: verum
end;
theorem :: FINSEQ_1:72
for p being FinSequence holds p | (Seg 0) = {} ;
theorem :: FINSEQ_1:73
for f, g being FinSequence holds f | (Seg 0) = g | (Seg 0) ;
theorem :: FINSEQ_1:74
for D being non empty set
for x being Element of D holds <*x*> is FinSequence of D ;
theorem :: FINSEQ_1:75
for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D ;
theorem :: FINSEQ_1:76
for a, b being set st <*a*> = <*b*> holds
a = b
proof
let a, b be set ; ::_thesis: ( <*a*> = <*b*> implies a = b )
assume A1: <*a*> = <*b*> ; ::_thesis: a = b
thus a = <*a*> . 1 by Def8
.= b by A1, Def8 ; ::_thesis: verum
end;
theorem :: FINSEQ_1:77
for a, b, c, d being set st <*a,b*> = <*c,d*> holds
( a = c & b = d )
proof
let a, b, c, d be set ; ::_thesis: ( <*a,b*> = <*c,d*> implies ( a = c & b = d ) )
assume A1: <*a,b*> = <*c,d*> ; ::_thesis: ( a = c & b = d )
thus a = <*a,b*> . 1 by Th44
.= c by A1, Th44 ; ::_thesis: b = d
thus b = <*a,b*> . 2 by Th44
.= d by A1, Th44 ; ::_thesis: verum
end;
theorem :: FINSEQ_1:78
for a, b, c, d, e, f being set st <*a,b,c*> = <*d,e,f*> holds
( a = d & b = e & c = f )
proof
let a, b, c, d, e, f be set ; ::_thesis: ( <*a,b,c*> = <*d,e,f*> implies ( a = d & b = e & c = f ) )
assume A1: <*a,b,c*> = <*d,e,f*> ; ::_thesis: ( a = d & b = e & c = f )
thus a = <*a,b,c*> . 1 by Th45
.= d by A1, Th45 ; ::_thesis: ( b = e & c = f )
thus b = <*a,b,c*> . 2 by Th45
.= e by A1, Th45 ; ::_thesis: c = f
thus c = <*a,b,c*> . 3 by Th45
.= f by A1, Th45 ; ::_thesis: verum
end;
registration
cluster Relation-like non-empty NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is non-empty )
proof
take <*{{}}*> ; ::_thesis: ( not <*{{}}*> is empty & <*{{}}*> is non-empty )
thus not <*{{}}*> is empty ; ::_thesis: <*{{}}*> is non-empty
assume {} in rng <*{{}}*> ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then {} in {{{}}} by Th38;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
end;
theorem Th79: :: FINSEQ_1:79
for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= len p
proof
let n be Nat; ::_thesis: for p, q being FinSequence st q = p | (Seg n) holds
len q <= len p
let p, q be FinSequence; ::_thesis: ( q = p | (Seg n) implies len q <= len p )
assume q = p | (Seg n) ; ::_thesis: len q <= len p
then A1: dom q = (dom p) /\ (Seg n) by RELAT_1:61;
( Seg (len q) = dom q & Seg (len p) = dom p ) by Def3;
then Seg (len q) c= Seg (len p) by A1, XBOOLE_1:17;
hence len q <= len p by Th5; ::_thesis: verum
end;
theorem :: FINSEQ_1:80
for n being Nat
for p, r being FinSequence st r = p | (Seg n) holds
ex q being FinSequence st p = r ^ q
proof
let n be Nat; ::_thesis: for p, r being FinSequence st r = p | (Seg n) holds
ex q being FinSequence st p = r ^ q
let p, r be FinSequence; ::_thesis: ( r = p | (Seg n) implies ex q being FinSequence st p = r ^ q )
assume A1: r = p | (Seg n) ; ::_thesis: ex q being FinSequence st p = r ^ q
then consider m being Nat such that
A2: len p = (len r) + m by Th79, NAT_1:10;
deffunc H1( Nat) -> set = p . ((len r) + $1);
consider q being FinSequence such that
A3: ( len q = m & ( for k being Nat st k in dom q holds
q . k = H1(k) ) ) from FINSEQ_1:sch_2();
take q ; ::_thesis: p = r ^ q
A4: len p = len (r ^ q) by A2, A3, Th22;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_p_holds_
p_._k_=_(r_^_q)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len p implies p . k = (r ^ q) . k )
assume that
A5: 1 <= k and
A6: k <= len p ; ::_thesis: p . k = (r ^ q) . k
A7: k in NAT by ORDINAL1:def_12;
A8: now__::_thesis:_(_k_<=_len_r_implies_p_._k_=_(r_^_q)_._k_)
assume k <= len r ; ::_thesis: p . k = (r ^ q) . k
then A9: k in Seg (len r) by A5, A7;
A10: dom r = Seg (len r) by Def3;
then (r ^ q) . k = r . k by A9, Def7;
hence p . k = (r ^ q) . k by A1, A9, A10, FUNCT_1:47; ::_thesis: verum
end;
now__::_thesis:_(_not_k_<=_len_r_implies_p_._k_=_(r_^_q)_._k_)
assume A11: not k <= len r ; ::_thesis: p . k = (r ^ q) . k
then consider j being Nat such that
A12: k = (len r) + j by NAT_1:10;
k - (len r) = j by A12;
then A13: (r ^ q) . k = q . j by A4, A6, A11, Th24;
j <> 0 by A11, A12;
then A14: 0 + 1 <= j by NAT_1:13;
j <= len q by A2, A3, A6, A12, XREAL_1:6;
then j in Seg m by A3, A14, Th1;
then j in dom q by A3, Def3;
hence p . k = (r ^ q) . k by A3, A12, A13; ::_thesis: verum
end;
hence p . k = (r ^ q) . k by A8; ::_thesis: verum
end;
hence p = r ^ q by A4, Th14; ::_thesis: verum
end;
registration
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like non empty finite FinSequence-like FinSubsequence-like for FinSequence of D;
existence
not for b1 being FinSequence of D holds b1 is empty
proof
set x = the Element of D;
take <* the Element of D*> ; ::_thesis: not <* the Element of D*> is empty
thus not <* the Element of D*> is empty ; ::_thesis: verum
end;
end;
definition
let p, q be FinSequence;
redefine pred p = q means :: FINSEQ_1:def 17
( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) );
compatibility
( p = q iff ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) ) ) by Th14;
end;
:: deftheorem defines = FINSEQ_1:def_17_:_
for p, q being FinSequence holds
( p = q iff ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) ) );
theorem :: FINSEQ_1:81
for M1, M2 being set st card M1 = 0 & card M2 = 0 holds
M1 = M2
proof
let M1, M2 be set ; ::_thesis: ( card M1 = 0 & card M2 = 0 implies M1 = M2 )
assume that
A1: card M1 = {} and
A2: card M2 = {} ; ::_thesis: M1 = M2
M1 = {} by A1;
hence M1 = M2 by A2; ::_thesis: verum
end;
registration
let n be non zero Nat;
cluster Seg n -> non empty ;
coherence
not Seg n is empty ;
end;
theorem :: FINSEQ_1:82
for p being FinSequence
for n, m being Nat st m <= n holds
(p | n) | m = p | m
proof
let p be FinSequence; ::_thesis: for n, m being Nat st m <= n holds
(p | n) | m = p | m
let n, m be Nat; ::_thesis: ( m <= n implies (p | n) | m = p | m )
assume m <= n ; ::_thesis: (p | n) | m = p | m
then Seg m c= Seg n by Th5;
hence (p | n) | m = p | m by RELAT_1:74; ::_thesis: verum
end;
theorem :: FINSEQ_1:83
for n being Nat holds Seg n = (n + 1) \ {0}
proof
let n be Nat; ::_thesis: Seg n = (n + 1) \ {0}
A1: n + 1 = { m where m is Element of NAT : m < n + 1 } by AXIOMS:4;
thus Seg n c= (n + 1) \ {0} :: according to XBOOLE_0:def_10 ::_thesis: (n + 1) \ {0} c= Seg n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg n or x in (n + 1) \ {0} )
assume x in Seg n ; ::_thesis: x in (n + 1) \ {0}
then consider k being Element of NAT such that
A2: x = k and
A3: 1 <= k and
A4: k <= n ;
k < n + 1 by A4, NAT_1:13;
then A5: x in n + 1 by A1, A2;
not x in {0} by A2, A3, TARSKI:def_1;
hence x in (n + 1) \ {0} by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (n + 1) \ {0} or x in Seg n )
assume A6: x in (n + 1) \ {0} ; ::_thesis: x in Seg n
then A7: x in n + 1 ;
A8: not x in {0} by A6, XBOOLE_0:def_5;
consider m being Element of NAT such that
A9: x = m and
A10: m < n + 1 by A1, A7;
A11: x <> 0 by A8, TARSKI:def_1;
0 + 1 = 1 ;
then A12: 1 <= m by A9, A11, NAT_1:13;
m <= n by A10, NAT_1:13;
hence x in Seg n by A9, A12; ::_thesis: verum
end;
registration
let n be Nat;
cluster Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st b1 is n -element
proof
set p = (Seg n) --> {};
dom ((Seg n) --> {}) = Seg n by FUNCOP_1:13;
then reconsider p = (Seg n) --> {} as FinSequence by Def2;
take p ; ::_thesis: p is n -element
Seg (len p) = dom p by Def3;
hence len p = n by Th6, FUNCOP_1:13; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
registration
let x be set ;
cluster<*x*> -> 1 -element ;
coherence
<*x*> is 1 -element ;
let y be set ;
cluster<*x,y*> -> 2 -element ;
coherence
<*x,y*> is 2 -element
proof
thus len <*x,y*> = 2 by Th44; :: according to CARD_1:def_7 ::_thesis: verum
end;
let z be set ;
cluster<*x,y,z*> -> 3 -element ;
coherence
<*x,y,z*> is 3 -element
proof
thus len <*x,y,z*> = 3 by Th45; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
definition
let X be set ;
attrX is FinSequence-membered means :Def18: :: FINSEQ_1:def 18
for x being set st x in X holds
x is FinSequence;
end;
:: deftheorem Def18 defines FinSequence-membered FINSEQ_1:def_18_:_
for X being set holds
( X is FinSequence-membered iff for x being set st x in X holds
x is FinSequence );
registration
cluster empty -> FinSequence-membered for set ;
coherence
for b1 being set st b1 is empty holds
b1 is FinSequence-membered
proof
let X be set ; ::_thesis: ( X is empty implies X is FinSequence-membered )
assume A1: X is empty ; ::_thesis: X is FinSequence-membered
let x be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( x in X implies x is FinSequence )
assume x in X ; ::_thesis: x is FinSequence
hence x is FinSequence by A1; ::_thesis: verum
end;
end;
registration
cluster non empty FinSequence-membered for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is FinSequence-membered )
proof
take X = { the FinSequence}; ::_thesis: ( not X is empty & X is FinSequence-membered )
thus not X is empty ; ::_thesis: X is FinSequence-membered
let x be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( x in X implies x is FinSequence )
thus ( x in X implies x is FinSequence ) by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let X be set ;
clusterX * -> FinSequence-membered ;
coherence
X * is FinSequence-membered
proof
let x be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( x in X * implies x is FinSequence )
assume x in X * ; ::_thesis: x is FinSequence
hence x is FinSequence by Def11; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:84
for x, D being set
for f being Function st f in D * & x in dom f holds
f . x in D
proof
let x, D be set ; ::_thesis: for f being Function st f in D * & x in dom f holds
f . x in D
let f be Function; ::_thesis: ( f in D * & x in dom f implies f . x in D )
assume that
A1: f in D * and
A2: x in dom f ; ::_thesis: f . x in D
f is FinSequence of D by A1, Def11;
then A3: rng f c= D by Def4;
f . x in rng f by A2, FUNCT_1:3;
hence f . x in D by A3; ::_thesis: verum
end;
registration
cluster FinSequence-membered -> functional for set ;
coherence
for b1 being set st b1 is FinSequence-membered holds
b1 is functional
proof
let X be set ; ::_thesis: ( X is FinSequence-membered implies X is functional )
assume A1: X is FinSequence-membered ; ::_thesis: X is functional
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in X or x is set )
assume x in X ; ::_thesis: x is set
hence x is Function by A1, Def18; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:85
for X being FinSequence-membered set ex Y being non empty set st X c= Y *
proof
let X be FinSequence-membered set ; ::_thesis: ex Y being non empty set st X c= Y *
set Z = { (rng f) where f is Element of X : f in X } ;
take Y = succ (union { (rng f) where f is Element of X : f in X } ); ::_thesis: X c= Y *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y * )
assume A1: x in X ; ::_thesis: x in Y *
then reconsider x = x as FinSequence by Def18;
rng x in { (rng f) where f is Element of X : f in X } by A1;
then rng x c= Y by ORDINAL3:1, SETFAM_1:41;
then x is FinSequence of Y by Def4;
hence x in Y * by Def11; ::_thesis: verum
end;
registration
let X be FinSequence-membered set ;
cluster -> FinSequence-like for Element of X;
coherence
for b1 being Element of X holds b1 is FinSequence-like
proof
let e be Element of X; ::_thesis: e is FinSequence-like
( X is empty or not X is empty ) ;
hence e is FinSequence-like by Def18, SUBSET_1:def_1; ::_thesis: verum
end;
end;
registration
let X be FinSequence-membered set ;
cluster -> FinSequence-membered for Element of bool X;
coherence
for b1 being Subset of X holds b1 is FinSequence-membered
proof
let Y be Subset of X; ::_thesis: Y is FinSequence-membered
let x be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( x in Y implies x is FinSequence )
assume x in Y ; ::_thesis: x is FinSequence
hence x is FinSequence ; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:86
for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= n
proof
let n be Nat; ::_thesis: for p, q being FinSequence st q = p | (Seg n) holds
len q <= n
let p, q be FinSequence; ::_thesis: ( q = p | (Seg n) implies len q <= n )
assume q = p | (Seg n) ; ::_thesis: len q <= n
then A1: dom q = (dom p) /\ (Seg n) by RELAT_1:61;
Seg (len q) = dom q by Def3;
then Seg (len q) c= Seg n by A1, XBOOLE_1:17;
hence len q <= n by Th5; ::_thesis: verum
end;
theorem :: FINSEQ_1:87
for p, q being FinSequence st ( p = p ^ q or p = q ^ p ) holds
q = {}
proof
let p, q be FinSequence; ::_thesis: ( ( p = p ^ q or p = q ^ p ) implies q = {} )
assume A1: ( p = p ^ q or p = q ^ p ) ; ::_thesis: q = {}
( len (p ^ q) = (len p) + (len q) & len (q ^ p) = (len q) + (len p) ) by Th22;
hence q = {} by A1; ::_thesis: verum
end;
theorem :: FINSEQ_1:88
for x being set
for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
proof
let x be set ; ::_thesis: for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
let p, q be FinSequence; ::_thesis: ( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
assume A1: p ^ q = <*x*> ; ::_thesis: ( ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
then A2: 1 = len (p ^ q) by Th40
.= (len p) + (len q) by Th22 ;
A3: now__::_thesis:_(_len_p_=_0_implies_(_p_=_{}_&_q_=_<*x*>_)_)
assume len p = 0 ; ::_thesis: ( p = {} & q = <*x*> )
hence p = {} ; ::_thesis: q = <*x*>
hence q = <*x*> by A1, Th34; ::_thesis: verum
end;
now__::_thesis:_(_len_p_<>_0_implies_(_q_=_{}_&_p_=_<*x*>_)_)
assume len p <> 0 ; ::_thesis: ( q = {} & p = <*x*> )
then A4: 0 + 1 <= len p by NAT_1:13;
len p <= 1 by A2, NAT_1:11;
then len p = 1 by A4, XXREAL_0:1;
hence q = {} by A2; ::_thesis: p = <*x*>
hence p = <*x*> by A1, Th34; ::_thesis: verum
end;
hence ( ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) ) by A3; ::_thesis: verum
end;
theorem :: FINSEQ_1:89
for n being Nat
for f being b1 -element FinSequence holds dom f = Seg n
proof
let n be Nat; ::_thesis: for f being n -element FinSequence holds dom f = Seg n
let f be n -element FinSequence; ::_thesis: dom f = Seg n
len f = n by CARD_1:def_7;
hence dom f = Seg n by Def3; ::_thesis: verum
end;
registration
let n be Nat;
let m be Element of NAT ;
let f be n -element FinSequence;
let g be m -element FinSequence;
clusterf ^ g -> n + m -element ;
coherence
f ^ g is n + m -element
proof
( len f = n & len g = m ) by CARD_1:def_7;
hence len (f ^ g) = n + m by Th22; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like real-valued increasing FinSequence-like -> one-to-one real-valued for set ;
coherence
for b1 being real-valued FinSequence st b1 is increasing holds
b1 is one-to-one
proof
let f be real-valued FinSequence; ::_thesis: ( f is increasing implies f is one-to-one )
assume A1: f is increasing ; ::_thesis: f is one-to-one
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A2: ( x in dom f & y in dom f ) and
A3: f . x = f . y ; ::_thesis: x = y
reconsider nx = x, ny = y as Element of NAT by A2;
( nx <= ny & nx >= ny ) by A1, A2, A3, VALUED_0:def_13;
hence x = y by XXREAL_0:1; ::_thesis: verum
end;
end;
theorem :: FINSEQ_1:90
for x, y being set st x in dom <*y*> holds
x = 1
proof
let x, y be set ; ::_thesis: ( x in dom <*y*> implies x = 1 )
assume x in dom <*y*> ; ::_thesis: x = 1
then x in Seg 1 by Th38;
hence x = 1 by Th2, TARSKI:def_1; ::_thesis: verum
end;
registration
let X be set ;
cluster Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st b1 is X -valued
proof
take <*> X ; ::_thesis: <*> X is X -valued
thus <*> X is X -valued ; ::_thesis: verum
end;
end;
registration
let D be FinSequence-membered set ;
let f be D -valued Function;
let x be set ;
clusterf . x -> FinSequence-like ;
coherence
f . x is FinSequence-like
proof
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . x is FinSequence-like
then A1: f . x in rng f by FUNCT_1:def_3;
rng f c= D by RELAT_1:def_19;
hence f . x is FinSequence-like by A1; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . x is FinSequence-like
hence f . x is FinSequence-like by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
end;