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