:: FINSEQ_5 semantic presentation begin theorem Th1: :: FINSEQ_5:1 for i, n being Nat st i <= n holds (n - i) + 1 is Element of NAT proof let i, n be Nat; ::_thesis: ( i <= n implies (n - i) + 1 is Element of NAT ) assume i <= n ; ::_thesis: (n - i) + 1 is Element of NAT then reconsider ni = n - i as Element of NAT by INT_1:5; ni + 1 is Element of NAT ; hence (n - i) + 1 is Element of NAT ; ::_thesis: verum end; theorem Th2: :: FINSEQ_5:2 for i, n being Nat st i in Seg n holds (n - i) + 1 in Seg n proof let i, n be Nat; ::_thesis: ( i in Seg n implies (n - i) + 1 in Seg n ) assume A1: i in Seg n ; ::_thesis: (n - i) + 1 in Seg n then i <= n by FINSEQ_1:1; then reconsider ni = n - i as Element of NAT by INT_1:5; reconsider j = ni + 1 as Element of NAT ; A2: now__::_thesis:_not_j_=_n_+_1 assume j = n + 1 ; ::_thesis: contradiction then - 0 = - i ; hence contradiction by A1, FINSEQ_1:1; ::_thesis: verum end; ni <= n by XREAL_1:43; then j <= n + 1 by XREAL_1:6; then j < n + 1 by A2, XXREAL_0:1; then ( 0 + 1 <= j & j <= n ) by NAT_1:13; hence (n - i) + 1 in Seg n ; ::_thesis: verum end; theorem Th3: :: FINSEQ_5:3 for f being Function for x, y being set st f " {y} = {x} holds ( x in dom f & y in rng f & f . x = y ) proof let f be Function; ::_thesis: for x, y being set st f " {y} = {x} holds ( x in dom f & y in rng f & f . x = y ) let x, y be set ; ::_thesis: ( f " {y} = {x} implies ( x in dom f & y in rng f & f . x = y ) ) assume f " {y} = {x} ; ::_thesis: ( x in dom f & y in rng f & f . x = y ) then A1: x in f " {y} by TARSKI:def_1; hence A2: x in dom f by FUNCT_1:def_7; ::_thesis: ( y in rng f & f . x = y ) f . x in {y} by A1, FUNCT_1:def_7; then f . x = y by TARSKI:def_1; hence ( y in rng f & f . x = y ) by A2, FUNCT_1:def_3; ::_thesis: verum end; theorem :: FINSEQ_5:4 for f being Function holds ( f is one-to-one iff for x being set st x in dom f holds f " {(f . x)} = {x} ) proof let f be Function; ::_thesis: ( f is one-to-one iff for x being set st x in dom f holds f " {(f . x)} = {x} ) now__::_thesis:_(_(_(_for_x_being_set_st_x_in_dom_f_holds_ f_is_one-to-one_at_x_)_implies_for_x_being_set_st_x_in_dom_f_holds_ f_"_{(f_._x)}_=_{x}_)_&_(_(_for_x_being_set_st_x_in_dom_f_holds_ f_"_{(f_._x)}_=_{x}_)_implies_for_x_being_set_st_x_in_dom_f_holds_ f_is_one-to-one_at_x_)_) hereby ::_thesis: ( ( for x being set st x in dom f holds f " {(f . x)} = {x} ) implies for x being set st x in dom f holds f is_one-to-one_at x ) assume A1: for x being set st x in dom f holds f is_one-to-one_at x ; ::_thesis: for x being set st x in dom f holds f " {(f . x)} = {x} let x be set ; ::_thesis: ( x in dom f implies f " {(f . x)} = {x} ) assume x in dom f ; ::_thesis: f " {(f . x)} = {x} then f is_one-to-one_at x by A1; hence f " {(f . x)} = {x} by FINSEQ_4:2; ::_thesis: verum end; assume A2: for x being set st x in dom f holds f " {(f . x)} = {x} ; ::_thesis: for x being set st x in dom f holds f is_one-to-one_at x let x be set ; ::_thesis: ( x in dom f implies f is_one-to-one_at x ) assume A3: x in dom f ; ::_thesis: f is_one-to-one_at x then f " {(f . x)} = {x} by A2; hence f is_one-to-one_at x by A3, FINSEQ_4:2; ::_thesis: verum end; hence ( f is one-to-one iff for x being set st x in dom f holds f " {(f . x)} = {x} ) by FINSEQ_4:4; ::_thesis: verum end; theorem :: FINSEQ_5:5 for f being Function for y1, y2 being set st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds y1 = y2 proof let f be Function; ::_thesis: for y1, y2 being set st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds y1 = y2 let y1, y2 be set ; ::_thesis: ( f is one-to-one & y1 in rng f & f " {y1} = f " {y2} implies y1 = y2 ) assume that A1: ( f is one-to-one & y1 in rng f ) and A2: f " {y1} = f " {y2} ; ::_thesis: y1 = y2 consider x1 being set such that A3: f " {y1} = {x1} by A1, FUNCT_1:74; f . x1 = y1 by A3, Th3; hence y1 = y2 by A2, A3, Th3; ::_thesis: verum end; registration let x be set ; cluster<*x*> -> trivial ; coherence <*x*> is trivial ; let y be set ; cluster<*x,y*> -> non trivial ; coherence not <*x,y*> is trivial proof len <*x,y*> = 2 by FINSEQ_1:44; hence not <*x,y*> is trivial by NAT_D:60; ::_thesis: verum end; end; registration cluster non empty Relation-like NAT -defined Function-like one-to-one V34() FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st ( b1 is one-to-one & not b1 is empty ) proof set f = <*{}*>; <*{}*> is one-to-one by FINSEQ_3:93; hence ex b1 being FinSequence st ( b1 is one-to-one & not b1 is empty ) ; ::_thesis: verum end; end; theorem Th6: :: FINSEQ_5:6 for f being non empty FinSequence holds ( 1 in dom f & len f in dom f ) proof let f be non empty FinSequence; ::_thesis: ( 1 in dom f & len f in dom f ) A1: len f >= 1 by NAT_1:14; hence 1 in dom f by FINSEQ_3:25; ::_thesis: len f in dom f thus len f in dom f by A1, FINSEQ_3:25; ::_thesis: verum end; theorem :: FINSEQ_5:7 for f being non empty FinSequence ex i being Nat st i + 1 = len f by NAT_1:6; theorem Th8: :: FINSEQ_5:8 for x being set for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f) proof let x be set ; ::_thesis: for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f) let f be FinSequence; ::_thesis: len (<*x*> ^ f) = 1 + (len f) thus len (<*x*> ^ f) = (len <*x*>) + (len f) by FINSEQ_1:22 .= 1 + (len f) by FINSEQ_1:39 ; ::_thesis: verum end; theorem :: FINSEQ_5:9 for f being FinSequence for p, q being set st p in rng f & q in rng f & p .. f = q .. f holds p = q proof let f be FinSequence; ::_thesis: for p, q being set st p in rng f & q in rng f & p .. f = q .. f holds p = q let p, q be set ; ::_thesis: ( p in rng f & q in rng f & p .. f = q .. f implies p = q ) assume that A1: p in rng f and A2: q in rng f ; ::_thesis: ( not p .. f = q .. f or p = q ) assume p .. f = q .. f ; ::_thesis: p = q hence p = f . (q .. f) by A1, FINSEQ_4:19 .= q by A2, FINSEQ_4:19 ; ::_thesis: verum end; theorem Th10: :: FINSEQ_5:10 for n being Nat for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> proof let n be Nat; ::_thesis: for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> let f, g be FinSequence; ::_thesis: ( n + 1 in dom f & g = f | (Seg n) implies f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> ) assume that A1: n + 1 in dom f and A2: g = f | (Seg n) ; ::_thesis: f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> reconsider h = f | (Seg (n + 1)) as FinSequence by FINSEQ_1:15; n + 1 <= len f by A1, FINSEQ_3:25; then A3: len h = n + 1 by FINSEQ_1:17; n <= n + 1 by NAT_1:11; then Seg n c= Seg (n + 1) by FINSEQ_1:5; then ( h . (n + 1) = f . (n + 1) & g = h | (Seg n) ) by A2, FINSEQ_1:4, FUNCT_1:49, FUNCT_1:51; hence f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> by A3, FINSEQ_3:55; ::_thesis: verum end; theorem Th11: :: FINSEQ_5:11 for i being Nat for f being one-to-one FinSequence st i in dom f holds (f . i) .. f = i proof let i be Nat; ::_thesis: for f being one-to-one FinSequence st i in dom f holds (f . i) .. f = i let f be one-to-one FinSequence; ::_thesis: ( i in dom f implies (f . i) .. f = i ) assume A1: i in dom f ; ::_thesis: (f . i) .. f = i then f . i in rng f by FUNCT_1:def_3; then A2: f just_once_values f . i by FINSEQ_4:8; then f <- (f . i) = (f . i) .. f by FINSEQ_4:25; hence (f . i) .. f = i by A1, A2, FINSEQ_4:def_3; ::_thesis: verum end; registration let D be non empty set ; cluster non empty Relation-like NAT -defined D -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is one-to-one & not b1 is empty ) proof set x = the Element of D; set f = <* the Element of D*>; <* the Element of D*> is one-to-one by FINSEQ_3:93; hence ex b1 being FinSequence of D st ( b1 is one-to-one & not b1 is empty ) ; ::_thesis: verum end; end; theorem :: FINSEQ_5:12 for D being non empty set for f, g being FinSequence of D st dom f = dom g & ( for i being Nat st i in dom f holds f /. i = g /. i ) holds f = g proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st dom f = dom g & ( for i being Nat st i in dom f holds f /. i = g /. i ) holds f = g let f, g be FinSequence of D; ::_thesis: ( dom f = dom g & ( for i being Nat st i in dom f holds f /. i = g /. i ) implies f = g ) assume that A1: dom f = dom g and A2: for i being Nat st i in dom f holds f /. i = g /. i ; ::_thesis: f = g now__::_thesis:_for_k_being_Nat_st_k_in_dom_f_holds_ f_._k_=_g_._k let k be Nat; ::_thesis: ( k in dom f implies f . k = g . k ) assume A3: k in dom f ; ::_thesis: f . k = g . k hence f . k = f /. k by PARTFUN1:def_6 .= g /. k by A2, A3 .= g . k by A1, A3, PARTFUN1:def_6 ; ::_thesis: verum end; hence f = g by A1, FINSEQ_1:13; ::_thesis: verum end; theorem Th13: :: FINSEQ_5:13 for D being non empty set for f, g being FinSequence of D st len f = len g & ( for k being Nat st 1 <= k & k <= len f holds f /. k = g /. k ) holds f = g proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st len f = len g & ( for k being Nat st 1 <= k & k <= len f holds f /. k = g /. k ) holds f = g let f, g be FinSequence of D; ::_thesis: ( len f = len g & ( for k being Nat st 1 <= k & k <= len f holds f /. k = g /. k ) implies f = g ) assume that A1: len f = len g and A2: for k being Nat st 1 <= k & k <= len f holds f /. k = g /. k ; ::_thesis: f = g now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_f_holds_ f_._k_=_g_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len f implies f . k = g . k ) assume A3: ( 1 <= k & k <= len f ) ; ::_thesis: f . k = g . k hence f . k = f /. k by FINSEQ_4:15 .= g /. k by A2, A3 .= g . k by A1, A3, FINSEQ_4:15 ; ::_thesis: verum end; hence f = g by A1, FINSEQ_1:14; ::_thesis: verum end; theorem Th14: :: FINSEQ_5:14 for D being non empty set for f being FinSequence of D st len f = 1 holds f = <*(f /. 1)*> proof let D be non empty set ; ::_thesis: for f being FinSequence of D st len f = 1 holds f = <*(f /. 1)*> let f be FinSequence of D; ::_thesis: ( len f = 1 implies f = <*(f /. 1)*> ) assume A1: len f = 1 ; ::_thesis: f = <*(f /. 1)*> then not f is empty ; then 1 in dom f by Th6; then f . 1 = f /. 1 by PARTFUN1:def_6; hence f = <*(f /. 1)*> by A1, FINSEQ_1:40; ::_thesis: verum end; theorem Th15: :: FINSEQ_5:15 for D being non empty set for p being Element of D for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p let p be Element of D; ::_thesis: for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p let f be FinSequence of D; ::_thesis: (<*p*> ^ f) /. 1 = p len (<*p*> ^ f) = 1 + (len f) by Th8; then 1 <= len (<*p*> ^ f) by NAT_1:11; then 1 in dom (<*p*> ^ f) by FINSEQ_3:25; then (<*p*> ^ f) /. 1 = (<*p*> ^ f) . 1 by PARTFUN1:def_6; hence (<*p*> ^ f) /. 1 = p by FINSEQ_1:41; ::_thesis: verum end; Lm1: for i being Nat for D being non empty set for f, g being FinSequence of D st i in dom f holds (f ^ g) /. i = f /. i proof let i be Nat; ::_thesis: for D being non empty set for f, g being FinSequence of D st i in dom f holds (f ^ g) /. i = f /. i let D be non empty set ; ::_thesis: for f, g being FinSequence of D st i in dom f holds (f ^ g) /. i = f /. i let f, g be FinSequence of D; ::_thesis: ( i in dom f implies (f ^ g) /. i = f /. i ) assume A1: i in dom f ; ::_thesis: (f ^ g) /. i = f /. i dom f c= dom (f ^ g) by FINSEQ_1:26; hence (f ^ g) /. i = (f ^ g) . i by A1, PARTFUN1:def_6 .= f . i by A1, FINSEQ_1:def_7 .= f /. i by A1, PARTFUN1:def_6 ; ::_thesis: verum end; theorem Th16: :: FINSEQ_5:16 for f being FinSequence for i being Nat holds len (f | i) <= len f proof let f be FinSequence; ::_thesis: for i being Nat holds len (f | i) <= len f let i be Nat; ::_thesis: len (f | i) <= len f ( i <= len f implies len (f | i) = i ) by FINSEQ_1:59; hence len (f | i) <= len f by FINSEQ_1:58; ::_thesis: verum end; theorem Th17: :: FINSEQ_5:17 for f being FinSequence for i being Nat holds len (f | i) <= i proof let f be FinSequence; ::_thesis: for i being Nat holds len (f | i) <= i let i be Nat; ::_thesis: len (f | i) <= i ( i <= len f implies len (f | i) = i ) by FINSEQ_1:59; hence len (f | i) <= i by FINSEQ_1:58; ::_thesis: verum end; theorem Th18: :: FINSEQ_5:18 for f being FinSequence for i being Nat holds dom (f | i) c= dom f proof let f be FinSequence; ::_thesis: for i being Nat holds dom (f | i) c= dom f let i be Nat; ::_thesis: dom (f | i) c= dom f f | i c= f by RELAT_1:59; hence dom (f | i) c= dom f by RELAT_1:11; ::_thesis: verum end; theorem Th19: :: FINSEQ_5:19 for f being FinSequence for i being Nat holds rng (f | i) c= rng f proof let f be FinSequence; ::_thesis: for i being Nat holds rng (f | i) c= rng f let i be Nat; ::_thesis: rng (f | i) c= rng f f | i c= f by RELAT_1:59; hence rng (f | i) c= rng f by RELAT_1:11; ::_thesis: verum end; theorem Th20: :: FINSEQ_5:20 for D being set for f being FinSequence of D st not f is empty holds f | 1 = <*(f /. 1)*> proof let D be set ; ::_thesis: for f being FinSequence of D st not f is empty holds f | 1 = <*(f /. 1)*> let f be FinSequence of D; ::_thesis: ( not f is empty implies f | 1 = <*(f /. 1)*> ) assume not f is empty ; ::_thesis: f | 1 = <*(f /. 1)*> then 1 in dom f by Th6; then 1 <= len f by FINSEQ_3:25; then A1: len (f | 1) = 1 by FINSEQ_1:59; then 1 in dom (f | 1) by FINSEQ_3:25; then ( (f | 1) /. 1 = (f | 1) . 1 & f /. 1 = (f | 1) /. 1 ) by FINSEQ_4:70, PARTFUN1:def_6; hence f | 1 = <*(f /. 1)*> by A1, FINSEQ_1:40; ::_thesis: verum end; theorem :: FINSEQ_5:21 for i being Nat for D being non empty set for f being FinSequence of D st i + 1 = len f holds f = (f | i) ^ <*(f /. (len f))*> proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st i + 1 = len f holds f = (f | i) ^ <*(f /. (len f))*> let D be non empty set ; ::_thesis: for f being FinSequence of D st i + 1 = len f holds f = (f | i) ^ <*(f /. (len f))*> let f be FinSequence of D; ::_thesis: ( i + 1 = len f implies f = (f | i) ^ <*(f /. (len f))*> ) assume A1: i + 1 = len f ; ::_thesis: f = (f | i) ^ <*(f /. (len f))*> then not f is empty ; then A2: i + 1 in dom f by A1, Th6; dom f = Seg (i + 1) by A1, FINSEQ_1:def_3; hence f = f | (Seg (i + 1)) by RELAT_1:68 .= (f | i) ^ <*(f . (i + 1))*> by A2, Th10 .= (f | i) ^ <*(f /. (len f))*> by A1, A2, PARTFUN1:def_6 ; ::_thesis: verum end; Lm2: for i being Nat for D being non empty set for f being FinSequence of D st f is one-to-one holds f | i is one-to-one proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st f is one-to-one holds f | i is one-to-one let D be non empty set ; ::_thesis: for f being FinSequence of D st f is one-to-one holds f | i is one-to-one let f be FinSequence of D; ::_thesis: ( f is one-to-one implies f | i is one-to-one ) assume A1: f is one-to-one ; ::_thesis: f | i is one-to-one now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_in_dom_(f_|_i)_&_m_in_dom_(f_|_i)_&_(f_|_i)_/._n_=_(f_|_i)_/._m_holds_ n_=_m A2: dom (f | i) c= dom f by Th18; let n, m be Element of NAT ; ::_thesis: ( n in dom (f | i) & m in dom (f | i) & (f | i) /. n = (f | i) /. m implies n = m ) assume that A3: n in dom (f | i) and A4: m in dom (f | i) and A5: (f | i) /. n = (f | i) /. m ; ::_thesis: n = m f /. n = (f | i) /. n by A3, FINSEQ_4:70 .= f /. m by A4, A5, FINSEQ_4:70 ; hence n = m by A1, A3, A4, A2, PARTFUN2:10; ::_thesis: verum end; hence f | i is one-to-one by PARTFUN2:9; ::_thesis: verum end; registration let i be Nat; let D be non empty set ; let f be one-to-one FinSequence of D; clusterf | i -> one-to-one ; coherence f | i is one-to-one by Lm2; end; theorem Th22: :: FINSEQ_5:22 for i being Nat for D being set for f, g being FinSequence of D st i <= len f holds (f ^ g) | i = f | i proof let i be Nat; ::_thesis: for D being set for f, g being FinSequence of D st i <= len f holds (f ^ g) | i = f | i let D be set ; ::_thesis: for f, g being FinSequence of D st i <= len f holds (f ^ g) | i = f | i let f, g be FinSequence of D; ::_thesis: ( i <= len f implies (f ^ g) | i = f | i ) assume A1: i <= len f ; ::_thesis: (f ^ g) | i = f | i then A2: len (f | i) = i by FINSEQ_1:59; then A3: dom (f | i) = Seg i by FINSEQ_1:def_3; A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(f_|_i)_holds_ ((f_^_g)_|_i)_._j_=_(f_|_i)_._j let j be Nat; ::_thesis: ( j in dom (f | i) implies ((f ^ g) | i) . j = (f | i) . j ) assume A5: j in dom (f | i) ; ::_thesis: ((f ^ g) | i) . j = (f | i) . j then j <= i by A3, FINSEQ_1:1; then A6: j <= len f by A1, XXREAL_0:2; ( j in NAT & 1 <= j ) by A3, A5, FINSEQ_1:1; then j in Seg (len f) by A6; then A7: j in dom f by FINSEQ_1:def_3; thus ((f ^ g) | i) . j = (f ^ g) . j by A3, A5, FUNCT_1:49 .= f . j by A7, FINSEQ_1:def_7 .= (f | i) . j by A3, A5, FUNCT_1:49 ; ::_thesis: verum end; i <= (len f) + (len g) by A1, NAT_1:12; then i <= len (f ^ g) by FINSEQ_1:22; then len ((f ^ g) | i) = i by FINSEQ_1:59; hence (f ^ g) | i = f | i by A2, A4, FINSEQ_2:9; ::_thesis: verum end; theorem :: FINSEQ_5:23 for D being set for f, g being FinSequence of D holds (f ^ g) | (len f) = f proof let D be set ; ::_thesis: for f, g being FinSequence of D holds (f ^ g) | (len f) = f let f, g be FinSequence of D; ::_thesis: (f ^ g) | (len f) = f thus f = f | (len f) by FINSEQ_2:20 .= (f ^ g) | (len f) by Th22 ; ::_thesis: verum end; theorem :: FINSEQ_5:24 for D being non empty set for p being Element of D for D being set for f being FinSequence of D st p in rng f holds (f -| p) ^ <*p*> = f | (p .. f) proof let D be non empty set ; ::_thesis: for p being Element of D for D being set for f being FinSequence of D st p in rng f holds (f -| p) ^ <*p*> = f | (p .. f) let p be Element of D; ::_thesis: for D being set for f being FinSequence of D st p in rng f holds (f -| p) ^ <*p*> = f | (p .. f) let D be set ; ::_thesis: for f being FinSequence of D st p in rng f holds (f -| p) ^ <*p*> = f | (p .. f) let f be FinSequence of D; ::_thesis: ( p in rng f implies (f -| p) ^ <*p*> = f | (p .. f) ) assume A1: p in rng f ; ::_thesis: (f -| p) ^ <*p*> = f | (p .. f) then consider n being Nat such that A2: n = (p .. f) - 1 and A3: f -| p = f | (Seg n) by FINSEQ_4:def_5; ( n + 1 in dom f & f . (n + 1) = p ) by A1, A2, FINSEQ_4:19, FINSEQ_4:20; hence (f -| p) ^ <*p*> = f | (p .. f) by A2, A3, Th10; ::_thesis: verum end; theorem :: FINSEQ_5:25 for i being Nat for D being non empty set for f being FinSequence of D holds len (f /^ i) <= len f proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D holds len (f /^ i) <= len f let D be non empty set ; ::_thesis: for f being FinSequence of D holds len (f /^ i) <= len f let f be FinSequence of D; ::_thesis: len (f /^ i) <= len f percases ( i <= len f or len f < i ) ; suppose i <= len f ; ::_thesis: len (f /^ i) <= len f then len (f /^ i) = (len f) - i by RFINSEQ:def_1; then (len (f /^ i)) + i = len f ; hence len (f /^ i) <= len f by NAT_1:11; ::_thesis: verum end; suppose len f < i ; ::_thesis: len (f /^ i) <= len f then f /^ i = <*> D by RFINSEQ:def_1; hence len (f /^ i) <= len f ; ::_thesis: verum end; end; end; theorem Th26: :: FINSEQ_5:26 for i, n being Nat for D being set for f being FinSequence of D st i in dom (f /^ n) holds n + i in dom f proof let i, n be Nat; ::_thesis: for D being set for f being FinSequence of D st i in dom (f /^ n) holds n + i in dom f let D be set ; ::_thesis: for f being FinSequence of D st i in dom (f /^ n) holds n + i in dom f let f be FinSequence of D; ::_thesis: ( i in dom (f /^ n) implies n + i in dom f ) assume A1: i in dom (f /^ n) ; ::_thesis: n + i in dom f percases ( n <= len f or n > len f ) ; supposeA2: n <= len f ; ::_thesis: n + i in dom f i <= len (f /^ n) by A1, FINSEQ_3:25; then i <= (len f) - n by A2, RFINSEQ:def_1; then A3: n + i <= len f by XREAL_1:19; ( 1 <= i & i <= i + n ) by A1, FINSEQ_3:25, NAT_1:11; then 1 <= i + n by XXREAL_0:2; hence n + i in dom f by A3, FINSEQ_3:25; ::_thesis: verum end; suppose n > len f ; ::_thesis: n + i in dom f then f /^ n = <*> D by RFINSEQ:def_1; hence n + i in dom f by A1; ::_thesis: verum end; end; end; theorem Th27: :: FINSEQ_5:27 for i, n being Nat for D being set for f being FinSequence of D st i in dom (f /^ n) holds (f /^ n) /. i = f /. (n + i) proof let i, n be Nat; ::_thesis: for D being set for f being FinSequence of D st i in dom (f /^ n) holds (f /^ n) /. i = f /. (n + i) let D be set ; ::_thesis: for f being FinSequence of D st i in dom (f /^ n) holds (f /^ n) /. i = f /. (n + i) let f be FinSequence of D; ::_thesis: ( i in dom (f /^ n) implies (f /^ n) /. i = f /. (n + i) ) assume A1: i in dom (f /^ n) ; ::_thesis: (f /^ n) /. i = f /. (n + i) percases ( n <= len f or n > len f ) ; supposeA2: n <= len f ; ::_thesis: (f /^ n) /. i = f /. (n + i) A3: n + i in dom f by A1, Th26; thus (f /^ n) /. i = (f /^ n) . i by A1, PARTFUN1:def_6 .= f . (n + i) by A1, A2, RFINSEQ:def_1 .= f /. (n + i) by A3, PARTFUN1:def_6 ; ::_thesis: verum end; suppose n > len f ; ::_thesis: (f /^ n) /. i = f /. (n + i) then f /^ n = <*> D by RFINSEQ:def_1; hence (f /^ n) /. i = f /. (n + i) by A1; ::_thesis: verum end; end; end; theorem Th28: :: FINSEQ_5:28 for D being set for f being FinSequence of D holds f /^ 0 = f proof let D be set ; ::_thesis: for f being FinSequence of D holds f /^ 0 = f let f be FinSequence of D; ::_thesis: f /^ 0 = f A1: 0 <= len f ; A2: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(f_/^_0)_holds_ (f_/^_0)_._i_=_f_._i let i be Nat; ::_thesis: ( 1 <= i & i <= len (f /^ 0) implies (f /^ 0) . i = f . i ) assume ( 1 <= i & i <= len (f /^ 0) ) ; ::_thesis: (f /^ 0) . i = f . i then i in dom (f /^ 0) by FINSEQ_3:25; hence (f /^ 0) . i = f . (i + 0) by A1, RFINSEQ:def_1 .= f . i ; ::_thesis: verum end; len (f /^ 0) = (len f) - 0 by RFINSEQ:def_1 .= len f ; hence f /^ 0 = f by A2, FINSEQ_1:14; ::_thesis: verum end; theorem :: FINSEQ_5:29 for D being non empty set for f being FinSequence of D st not f is empty holds f = <*(f /. 1)*> ^ (f /^ 1) proof let D be non empty set ; ::_thesis: for f being FinSequence of D st not f is empty holds f = <*(f /. 1)*> ^ (f /^ 1) let f be FinSequence of D; ::_thesis: ( not f is empty implies f = <*(f /. 1)*> ^ (f /^ 1) ) assume not f is empty ; ::_thesis: f = <*(f /. 1)*> ^ (f /^ 1) then f | 1 = <*(f /. 1)*> by Th20; hence f = <*(f /. 1)*> ^ (f /^ 1) by RFINSEQ:8; ::_thesis: verum end; theorem :: FINSEQ_5:30 for i being Nat for D being non empty set for f being FinSequence of D st i + 1 = len f holds f /^ i = <*(f /. (len f))*> proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st i + 1 = len f holds f /^ i = <*(f /. (len f))*> let D be non empty set ; ::_thesis: for f being FinSequence of D st i + 1 = len f holds f /^ i = <*(f /. (len f))*> let f be FinSequence of D; ::_thesis: ( i + 1 = len f implies f /^ i = <*(f /. (len f))*> ) assume A1: i + 1 = len f ; ::_thesis: f /^ i = <*(f /. (len f))*> then i <= len f by NAT_1:11; then A2: len (f /^ i) = (len f) - i by RFINSEQ:def_1 .= 1 by A1 ; then A3: 1 in dom (f /^ i) by FINSEQ_3:25; thus f /^ i = <*((f /^ i) /. 1)*> by A2, Th14 .= <*(f /. (len f))*> by A1, A3, Th27 ; ::_thesis: verum end; theorem Th31: :: FINSEQ_5:31 for j, i being Nat for D being non empty set for f being FinSequence of D st j + 1 = i & i in dom f holds <*(f /. i)*> ^ (f /^ i) = f /^ j proof let j, i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st j + 1 = i & i in dom f holds <*(f /. i)*> ^ (f /^ i) = f /^ j let D be non empty set ; ::_thesis: for f being FinSequence of D st j + 1 = i & i in dom f holds <*(f /. i)*> ^ (f /^ i) = f /^ j let f be FinSequence of D; ::_thesis: ( j + 1 = i & i in dom f implies <*(f /. i)*> ^ (f /^ i) = f /^ j ) assume that A1: j + 1 = i and A2: i in dom f ; ::_thesis: <*(f /. i)*> ^ (f /^ i) = f /^ j set g = <*(f /. i)*> ^ (f /^ i); A3: i <= len f by A2, FINSEQ_3:25; j <= i by A1, NAT_1:11; then A4: j <= len f by A3, XXREAL_0:2; A5: len (<*(f /. i)*> ^ (f /^ i)) = (len (f /^ i)) + 1 by Th8; then A6: len (<*(f /. i)*> ^ (f /^ i)) = ((len f) - i) + 1 by A3, RFINSEQ:def_1 .= (len f) - j by A1 .= len (f /^ j) by A4, RFINSEQ:def_1 ; now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(<*(f_/._i)*>_^_(f_/^_i))_holds_ (<*(f_/._i)*>_^_(f_/^_i))_._k_=_(f_/^_j)_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len (<*(f /. i)*> ^ (f /^ i)) implies (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1 ) assume that A7: 1 <= k and A8: k <= len (<*(f /. i)*> ^ (f /^ i)) ; ::_thesis: (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1 A9: k in dom (f /^ j) by A6, A7, A8, FINSEQ_3:25; percases ( k = 1 or k <> 1 ) ; supposeA10: k = 1 ; ::_thesis: (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1 hence (<*(f /. i)*> ^ (f /^ i)) . k = f /. i by FINSEQ_1:41 .= f . i by A2, PARTFUN1:def_6 .= (f /^ j) . k by A1, A4, A9, A10, RFINSEQ:def_1 ; ::_thesis: verum end; suppose k <> 1 ; ::_thesis: (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1 then A11: 1 < k by A7, XXREAL_0:1; reconsider k9 = k - 1 as Element of NAT by A7, INT_1:5; A12: k9 <= (len (<*(f /. i)*> ^ (f /^ i))) - 1 by A8, XREAL_1:9; k9 + 1 = k ; then 1 <= k9 by A11, NAT_1:13; then A13: k9 in dom (f /^ i) by A5, A12, FINSEQ_3:25; len <*(f /. i)*> = 1 by FINSEQ_1:39; hence (<*(f /. i)*> ^ (f /^ i)) . k = (f /^ i) . k9 by A8, A11, FINSEQ_1:24 .= f . (k9 + i) by A3, A13, RFINSEQ:def_1 .= f . (k + j) by A1 .= (f /^ j) . k by A4, A9, RFINSEQ:def_1 ; ::_thesis: verum end; end; end; hence <*(f /. i)*> ^ (f /^ i) = f /^ j by A6, FINSEQ_1:14; ::_thesis: verum end; theorem Th32: :: FINSEQ_5:32 for i being Nat for D being set for f being FinSequence of D st len f <= i holds f /^ i is empty proof let i be Nat; ::_thesis: for D being set for f being FinSequence of D st len f <= i holds f /^ i is empty let D be set ; ::_thesis: for f being FinSequence of D st len f <= i holds f /^ i is empty let f be FinSequence of D; ::_thesis: ( len f <= i implies f /^ i is empty ) assume A1: len f <= i ; ::_thesis: f /^ i is empty percases ( len f = i or len f <> i ) ; suppose len f = i ; ::_thesis: f /^ i is empty then len (f /^ i) = (len f) - (len f) by RFINSEQ:def_1 .= 0 ; hence f /^ i is empty ; ::_thesis: verum end; suppose len f <> i ; ::_thesis: f /^ i is empty then len f < i by A1, XXREAL_0:1; hence f /^ i is empty by RFINSEQ:def_1; ::_thesis: verum end; end; end; theorem Th33: :: FINSEQ_5:33 for n being Nat for D being non empty set for f being FinSequence of D holds rng (f /^ n) c= rng f proof let n be Nat; ::_thesis: for D being non empty set for f being FinSequence of D holds rng (f /^ n) c= rng f let D be non empty set ; ::_thesis: for f being FinSequence of D holds rng (f /^ n) c= rng f let f be FinSequence of D; ::_thesis: rng (f /^ n) c= rng f let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in rng (f /^ n) or p in rng f ) assume p in rng (f /^ n) ; ::_thesis: p in rng f then consider j being Element of NAT such that A1: j in dom (f /^ n) and A2: (f /^ n) /. j = p by PARTFUN2:2; j + n in dom f by A1, Th26; then f /. (j + n) in rng f by PARTFUN2:2; hence p in rng f by A1, A2, Th27; ::_thesis: verum end; Lm3: for i being Nat for D being non empty set for f being FinSequence of D st f is one-to-one holds f /^ i is one-to-one proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st f is one-to-one holds f /^ i is one-to-one let D be non empty set ; ::_thesis: for f being FinSequence of D st f is one-to-one holds f /^ i is one-to-one let f be FinSequence of D; ::_thesis: ( f is one-to-one implies f /^ i is one-to-one ) assume A1: f is one-to-one ; ::_thesis: f /^ i is one-to-one now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_in_dom_(f_/^_i)_&_m_in_dom_(f_/^_i)_&_(f_/^_i)_/._n_=_(f_/^_i)_/._m_holds_ n_=_m let n, m be Element of NAT ; ::_thesis: ( n in dom (f /^ i) & m in dom (f /^ i) & (f /^ i) /. n = (f /^ i) /. m implies n = m ) assume that A2: n in dom (f /^ i) and A3: m in dom (f /^ i) and A4: (f /^ i) /. n = (f /^ i) /. m ; ::_thesis: n = m A5: ( i + n in dom f & i + m in dom f ) by A2, A3, Th26; f /. (i + n) = (f /^ i) /. n by A2, Th27 .= f /. (i + m) by A3, A4, Th27 ; then i + n = i + m by A1, A5, PARTFUN2:10; hence n = m ; ::_thesis: verum end; hence f /^ i is one-to-one by PARTFUN2:9; ::_thesis: verum end; registration let i be Nat; let D be non empty set ; let f be one-to-one FinSequence of D; clusterf /^ i -> one-to-one ; coherence f /^ i is one-to-one by Lm3; end; theorem Th34: :: FINSEQ_5:34 for n being Nat for D being non empty set for f being FinSequence of D st f is one-to-one holds rng (f | n) misses rng (f /^ n) proof let n be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st f is one-to-one holds rng (f | n) misses rng (f /^ n) let D be non empty set ; ::_thesis: for f being FinSequence of D st f is one-to-one holds rng (f | n) misses rng (f /^ n) let f be FinSequence of D; ::_thesis: ( f is one-to-one implies rng (f | n) misses rng (f /^ n) ) assume A1: f is one-to-one ; ::_thesis: rng (f | n) misses rng (f /^ n) A2: dom (f | n) c= dom f by Th18; assume rng (f | n) meets rng (f /^ n) ; ::_thesis: contradiction then consider x being set such that A3: x in rng (f | n) and A4: x in rng (f /^ n) by XBOOLE_0:3; consider i being Element of NAT such that A5: i in dom (f | n) and A6: (f | n) /. i = x by A3, PARTFUN2:2; consider j being Element of NAT such that A7: j in dom (f /^ n) and A8: (f /^ n) /. j = x by A4, PARTFUN2:2; A9: j + n in dom f by A7, Th26; A10: now__::_thesis:_not_i_=_j_+_n ( i <= len (f | n) & len (f | n) <= n ) by A5, Th17, FINSEQ_3:25; then A11: i <= n by XXREAL_0:2; assume A12: i = j + n ; ::_thesis: contradiction then n <= i by NAT_1:11; then i = n by A11, XXREAL_0:1; then j = 0 by A12; hence contradiction by A7, FINSEQ_3:25; ::_thesis: verum end; f /. (j + n) = (f /^ n) /. j by A7, Th27 .= f /. i by A5, A6, A8, FINSEQ_4:70 ; hence contradiction by A1, A5, A2, A9, A10, PARTFUN2:10; ::_thesis: verum end; theorem :: FINSEQ_5:35 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds f |-- p = f /^ (p .. f) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds f |-- p = f /^ (p .. f) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds f |-- p = f /^ (p .. f) let f be FinSequence of D; ::_thesis: ( p in rng f implies f |-- p = f /^ (p .. f) ) assume A1: p in rng f ; ::_thesis: f |-- p = f /^ (p .. f) then A2: len (f |-- p) = (len f) - (p .. f) by FINSEQ_4:def_6; A3: p .. f <= len f by A1, FINSEQ_4:21; then A4: len (f /^ (p .. f)) = (len f) - (p .. f) by RFINSEQ:def_1; A5: ( Seg (len (f |-- p)) = dom (f |-- p) & Seg (len (f /^ (p .. f))) = dom (f /^ (p .. f)) ) by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(f_|--_p)_holds_ (f_|--_p)_._i_=_(f_/^_(p_.._f))_._i let i be Nat; ::_thesis: ( i in dom (f |-- p) implies (f |-- p) . i = (f /^ (p .. f)) . i ) assume A6: i in dom (f |-- p) ; ::_thesis: (f |-- p) . i = (f /^ (p .. f)) . i hence (f |-- p) . i = f . (i + (p .. f)) by A1, FINSEQ_4:def_6 .= (f /^ (p .. f)) . i by A2, A3, A4, A5, A6, RFINSEQ:def_1 ; ::_thesis: verum end; hence f |-- p = f /^ (p .. f) by A2, A4, FINSEQ_2:9; ::_thesis: verum end; theorem Th36: :: FINSEQ_5:36 for i being Nat for D being non empty set for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i proof let i be Nat; ::_thesis: for D being non empty set for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i let f, g be FinSequence of D; ::_thesis: (f ^ g) /^ ((len f) + i) = g /^ i A1: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; percases ( i <= len g or i > len g ) ; supposeA2: i <= len g ; ::_thesis: (f ^ g) /^ ((len f) + i) = g /^ i then (len f) + i <= (len f) + (len g) by XREAL_1:6; then A3: len ((f ^ g) /^ ((len f) + i)) = ((len g) + (len f)) - ((len f) + i) by A1, RFINSEQ:def_1 .= (len g) - i .= len (g /^ i) by A2, RFINSEQ:def_1 ; now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(g_/^_i)_holds_ ((f_^_g)_/^_((len_f)_+_i))_/._k_=_(g_/^_i)_/._k let k be Nat; ::_thesis: ( 1 <= k & k <= len (g /^ i) implies ((f ^ g) /^ ((len f) + i)) /. k = (g /^ i) /. k ) assume A4: ( 1 <= k & k <= len (g /^ i) ) ; ::_thesis: ((f ^ g) /^ ((len f) + i)) /. k = (g /^ i) /. k then A5: k in dom (g /^ i) by FINSEQ_3:25; then A6: i + k in dom g by Th26; k in dom ((f ^ g) /^ ((len f) + i)) by A3, A4, FINSEQ_3:25; hence ((f ^ g) /^ ((len f) + i)) /. k = (f ^ g) /. (((len f) + i) + k) by Th27 .= (f ^ g) /. ((len f) + (i + k)) .= g /. (i + k) by A6, FINSEQ_4:69 .= (g /^ i) /. k by A5, Th27 ; ::_thesis: verum end; hence (f ^ g) /^ ((len f) + i) = g /^ i by A3, Th13; ::_thesis: verum end; supposeA7: i > len g ; ::_thesis: (f ^ g) /^ ((len f) + i) = g /^ i then (len f) + i > len (f ^ g) by A1, XREAL_1:6; hence (f ^ g) /^ ((len f) + i) = <*> D by RFINSEQ:def_1 .= g /^ i by A7, RFINSEQ:def_1 ; ::_thesis: verum end; end; end; theorem :: FINSEQ_5:37 for D being non empty set for f, g being FinSequence of D holds (f ^ g) /^ (len f) = g proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds (f ^ g) /^ (len f) = g let f, g be FinSequence of D; ::_thesis: (f ^ g) /^ (len f) = g thus (f ^ g) /^ (len f) = (f ^ g) /^ ((len f) + 0) .= g /^ 0 by Th36 .= g by Th28 ; ::_thesis: verum end; theorem Th38: :: FINSEQ_5:38 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds f /. (p .. f) = p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds f /. (p .. f) = p let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds f /. (p .. f) = p let f be FinSequence of D; ::_thesis: ( p in rng f implies f /. (p .. f) = p ) assume p in rng f ; ::_thesis: f /. (p .. f) = p then ( p .. f in dom f & f . (p .. f) = p ) by FINSEQ_4:19, FINSEQ_4:20; hence f /. (p .. f) = p by PARTFUN1:def_6; ::_thesis: verum end; theorem Th39: :: FINSEQ_5:39 for i being Nat for D being non empty set for f being FinSequence of D st i in dom f holds (f /. i) .. f <= i proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st i in dom f holds (f /. i) .. f <= i let D be non empty set ; ::_thesis: for f being FinSequence of D st i in dom f holds (f /. i) .. f <= i let f be FinSequence of D; ::_thesis: ( i in dom f implies (f /. i) .. f <= i ) set p = f /. i; A1: (f /. i) .. f = (Sgm (f " {(f /. i)})) . 1 by FINSEQ_4:def_4; f " {(f /. i)} c= dom f by RELAT_1:132; then A2: f " {(f /. i)} c= Seg (len f) by FINSEQ_1:def_3; assume A3: i in dom f ; ::_thesis: (f /. i) .. f <= i then f /. i = f . i by PARTFUN1:def_6; then f . i in {(f /. i)} by TARSKI:def_1; then i in f " {(f /. i)} by A3, FUNCT_1:def_7; then i in rng (Sgm (f " {(f /. i)})) by A2, FINSEQ_1:def_13; then consider l being set such that A4: l in dom (Sgm (f " {(f /. i)})) and A5: (Sgm (f " {(f /. i)})) . l = i by FUNCT_1:def_3; reconsider l = l as Element of NAT by A4; ( 1 <= l & l <= len (Sgm (f " {(f /. i)})) ) by A4, FINSEQ_3:25; hence (f /. i) .. f <= i by A1, A2, A5, FINSEQ_3:41; ::_thesis: verum end; theorem :: FINSEQ_5:40 for i being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng (f | i) holds p .. (f | i) = p .. f proof let i be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng (f | i) holds p .. (f | i) = p .. f let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng (f | i) holds p .. (f | i) = p .. f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng (f | i) holds p .. (f | i) = p .. f let f be FinSequence of D; ::_thesis: ( p in rng (f | i) implies p .. (f | i) = p .. f ) A1: dom (f | i) c= dom f by Th18; assume A2: p in rng (f | i) ; ::_thesis: p .. (f | i) = p .. f then A3: p .. (f | i) in dom (f | i) by FINSEQ_4:20; then f /. (p .. (f | i)) = (f | i) /. (p .. (f | i)) by FINSEQ_4:70 .= p by A2, Th38 ; then A4: p .. f <= p .. (f | i) by A3, A1, Th39; p .. (f | i) <= len (f | i) by A2, FINSEQ_4:21; then A5: p .. f <= len (f | i) by A4, XXREAL_0:2; A6: rng (f | i) c= rng f by Th19; then 1 <= p .. f by A2, FINSEQ_4:21; then A7: p .. f in dom (f | i) by A5, FINSEQ_3:25; then (f | i) /. (p .. f) = f /. (p .. f) by FINSEQ_4:70 .= p by A2, A6, Th38 ; then p .. (f | i) <= p .. f by A7, Th39; hence p .. (f | i) = p .. f by A4, XXREAL_0:1; ::_thesis: verum end; theorem :: FINSEQ_5:41 for i being Nat for D being non empty set for f being FinSequence of D st i in dom f & f is one-to-one holds (f /. i) .. f = i proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st i in dom f & f is one-to-one holds (f /. i) .. f = i let D be non empty set ; ::_thesis: for f being FinSequence of D st i in dom f & f is one-to-one holds (f /. i) .. f = i let f be FinSequence of D; ::_thesis: ( i in dom f & f is one-to-one implies (f /. i) .. f = i ) assume A1: i in dom f ; ::_thesis: ( not f is one-to-one or (f /. i) .. f = i ) assume f is one-to-one ; ::_thesis: (f /. i) .. f = i then (f . i) .. f = i by A1, Th11; hence (f /. i) .. f = i by A1, PARTFUN1:def_6; ::_thesis: verum end; definition let D be non empty set ; let f be FinSequence of D; let p be set ; funcf -: p -> FinSequence of D equals :: FINSEQ_5:def 1 f | (p .. f); correctness coherence f | (p .. f) is FinSequence of D; ; end; :: deftheorem defines -: FINSEQ_5:def_1_:_ for D being non empty set for f being FinSequence of D for p being set holds f -: p = f | (p .. f); theorem Th42: :: FINSEQ_5:42 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds len (f -: p) = p .. f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds len (f -: p) = p .. f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds len (f -: p) = p .. f let f be FinSequence of D; ::_thesis: ( p in rng f implies len (f -: p) = p .. f ) assume p in rng f ; ::_thesis: len (f -: p) = p .. f then p .. f in dom f by FINSEQ_4:20; then p .. f <= len f by FINSEQ_3:25; hence len (f -: p) = p .. f by FINSEQ_1:59; ::_thesis: verum end; theorem Th43: :: FINSEQ_5:43 for i being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds (f -: p) /. i = f /. i proof let i be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds (f -: p) /. i = f /. i let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds (f -: p) /. i = f /. i let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds (f -: p) /. i = f /. i let f be FinSequence of D; ::_thesis: ( p in rng f & i in Seg (p .. f) implies (f -: p) /. i = f /. i ) assume that A1: p in rng f and A2: i in Seg (p .. f) ; ::_thesis: (f -: p) /. i = f /. i p .. f in dom f by A1, FINSEQ_4:20; hence (f -: p) /. i = f /. i by A2, FINSEQ_4:71; ::_thesis: verum end; theorem :: FINSEQ_5:44 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) /. 1 = f /. 1 proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) /. 1 = f /. 1 let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds (f -: p) /. 1 = f /. 1 let f be FinSequence of D; ::_thesis: ( p in rng f implies (f -: p) /. 1 = f /. 1 ) assume A1: p in rng f ; ::_thesis: (f -: p) /. 1 = f /. 1 then 1 <= p .. f by FINSEQ_4:21; then 1 in Seg (p .. f) ; hence (f -: p) /. 1 = f /. 1 by A1, Th43; ::_thesis: verum end; theorem :: FINSEQ_5:45 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) /. (p .. f) = p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) /. (p .. f) = p let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds (f -: p) /. (p .. f) = p let f be FinSequence of D; ::_thesis: ( p in rng f implies (f -: p) /. (p .. f) = p ) assume A1: p in rng f ; ::_thesis: (f -: p) /. (p .. f) = p then A2: p .. f in dom f by FINSEQ_4:20; 1 <= p .. f by A1, FINSEQ_4:21; then p .. f in Seg (p .. f) ; hence (f -: p) /. (p .. f) = f /. (p .. f) by A1, Th43 .= f . (p .. f) by A2, PARTFUN1:def_6 .= p by A1, FINSEQ_4:19 ; ::_thesis: verum end; theorem :: FINSEQ_5:46 for D being non empty set for p being Element of D for f being FinSequence of D for x being set st x in rng f & p in rng f & x .. f <= p .. f holds x in rng (f -: p) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D for x being set st x in rng f & p in rng f & x .. f <= p .. f holds x in rng (f -: p) let p be Element of D; ::_thesis: for f being FinSequence of D for x being set st x in rng f & p in rng f & x .. f <= p .. f holds x in rng (f -: p) let f be FinSequence of D; ::_thesis: for x being set st x in rng f & p in rng f & x .. f <= p .. f holds x in rng (f -: p) let x be set ; ::_thesis: ( x in rng f & p in rng f & x .. f <= p .. f implies x in rng (f -: p) ) assume that A1: x in rng f and A2: p in rng f and A3: x .. f <= p .. f ; ::_thesis: x in rng (f -: p) set g = f -: p; set i = x .. f; 1 <= x .. f by A1, FINSEQ_4:21; then A4: x .. f in Seg (p .. f) by A3; Seg (len (f -: p)) = dom (f -: p) by FINSEQ_1:def_3; then A5: x .. f in dom (f -: p) by A2, A4, Th42; then (f -: p) . (x .. f) in rng (f -: p) by FUNCT_1:def_3; then (f -: p) /. (x .. f) in rng (f -: p) by A5, PARTFUN1:def_6; then A6: f /. (x .. f) in rng (f -: p) by A2, A4, Th43; x .. f in dom f by A1, FINSEQ_4:20; then f . (x .. f) in rng (f -: p) by A6, PARTFUN1:def_6; hence x in rng (f -: p) by A1, FINSEQ_4:19; ::_thesis: verum end; theorem :: FINSEQ_5:47 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds not f -: p is empty proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds not f -: p is empty let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds not f -: p is empty let f be FinSequence of D; ::_thesis: ( p in rng f implies not f -: p is empty ) assume A1: p in rng f ; ::_thesis: not f -: p is empty then 1 <= p .. f by FINSEQ_4:21; then 1 <= len (f -: p) by A1, Th42; hence not f -: p is empty ; ::_thesis: verum end; theorem :: FINSEQ_5:48 for D being non empty set for p being Element of D for f being FinSequence of D holds rng (f -: p) c= rng f by Th19; registration let D be non empty set ; let p be Element of D; let f be one-to-one FinSequence of D; clusterf -: p -> one-to-one ; coherence f -: p is one-to-one ; end; definition let D be non empty set ; let f be FinSequence of D; let p be Element of D; funcf :- p -> FinSequence of D equals :: FINSEQ_5:def 2 <*p*> ^ (f /^ (p .. f)); coherence <*p*> ^ (f /^ (p .. f)) is FinSequence of D ; end; :: deftheorem defines :- FINSEQ_5:def_2_:_ for D being non empty set for f being FinSequence of D for p being Element of D holds f :- p = <*p*> ^ (f /^ (p .. f)); theorem Th49: :: FINSEQ_5:49 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) let f be FinSequence of D; ::_thesis: ( p in rng f implies ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) ) assume A1: p in rng f ; ::_thesis: ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) then reconsider i = (p .. f) - 1 as Element of NAT by FINSEQ_4:21, INT_1:5; A2: p .. f in dom f by A1, FINSEQ_4:20; take i ; ::_thesis: ( i + 1 = p .. f & f :- p = f /^ i ) thus A3: i + 1 = p .. f ; ::_thesis: f :- p = f /^ i thus f :- p = <*(f /. (p .. f))*> ^ (f /^ (p .. f)) by A1, Th38 .= f /^ i by A3, A2, Th31 ; ::_thesis: verum end; theorem Th50: :: FINSEQ_5:50 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds len (f :- p) = ((len f) - (p .. f)) + 1 proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds len (f :- p) = ((len f) - (p .. f)) + 1 let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds len (f :- p) = ((len f) - (p .. f)) + 1 let f be FinSequence of D; ::_thesis: ( p in rng f implies len (f :- p) = ((len f) - (p .. f)) + 1 ) assume A1: p in rng f ; ::_thesis: len (f :- p) = ((len f) - (p .. f)) + 1 then A2: p .. f <= len f by FINSEQ_4:21; consider i being Element of NAT such that A3: i + 1 = p .. f and A4: f :- p = f /^ i by A1, Th49; i <= p .. f by A3, NAT_1:11; then i <= len f by A2, XXREAL_0:2; hence len (f :- p) = (len f) - i by A4, RFINSEQ:def_1 .= ((len f) - (p .. f)) + 1 by A3 ; ::_thesis: verum end; theorem Th51: :: FINSEQ_5:51 for j being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds j + (p .. f) in dom f proof let j be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds j + (p .. f) in dom f let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds j + (p .. f) in dom f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds j + (p .. f) in dom f let f be FinSequence of D; ::_thesis: ( p in rng f & j + 1 in dom (f :- p) implies j + (p .. f) in dom f ) assume that A1: p in rng f and A2: j + 1 in dom (f :- p) ; ::_thesis: j + (p .. f) in dom f j + 1 <= len (f :- p) by A2, FINSEQ_3:25; then j + 1 <= ((len f) - (p .. f)) + 1 by A1, Th50; then j <= (len f) - (p .. f) by XREAL_1:6; then A3: j + (p .. f) <= len f by XREAL_1:19; A4: p .. f <= j + (p .. f) by NAT_1:11; 1 <= p .. f by A1, FINSEQ_4:21; then 1 <= j + (p .. f) by A4, XXREAL_0:2; hence j + (p .. f) in dom f by A3, FINSEQ_3:25; ::_thesis: verum end; registration let D be non empty set ; let p be Element of D; let f be FinSequence of D; clusterf :- p -> non empty ; coherence not f :- p is empty ; end; theorem Th52: :: FINSEQ_5:52 for j being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds (f :- p) /. (j + 1) = f /. (j + (p .. f)) proof let j be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds (f :- p) /. (j + 1) = f /. (j + (p .. f)) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds (f :- p) /. (j + 1) = f /. (j + (p .. f)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds (f :- p) /. (j + 1) = f /. (j + (p .. f)) let f be FinSequence of D; ::_thesis: ( p in rng f & j + 1 in dom (f :- p) implies (f :- p) /. (j + 1) = f /. (j + (p .. f)) ) assume that A1: p in rng f and A2: j + 1 in dom (f :- p) ; ::_thesis: (f :- p) /. (j + 1) = f /. (j + (p .. f)) A3: j + (p .. f) in dom f by A1, A2, Th51; set i = j + 1; A4: p .. f <= len f by A1, FINSEQ_4:21; consider k being Element of NAT such that A5: k + 1 = p .. f and A6: f :- p = f /^ k by A1, Th49; k <= p .. f by A5, NAT_1:11; then A7: k <= len f by A4, XXREAL_0:2; thus (f :- p) /. (j + 1) = (f :- p) . (j + 1) by A2, PARTFUN1:def_6 .= f . ((j + 1) + k) by A2, A6, A7, RFINSEQ:def_1 .= f /. (j + (p .. f)) by A5, A3, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: FINSEQ_5:53 for D being non empty set for p being Element of D for f being FinSequence of D holds (f :- p) /. 1 = p by Th15; theorem :: FINSEQ_5:54 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (f :- p) /. (len (f :- p)) = f /. (len f) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds (f :- p) /. (len (f :- p)) = f /. (len f) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds (f :- p) /. (len (f :- p)) = f /. (len f) let f be FinSequence of D; ::_thesis: ( p in rng f implies (f :- p) /. (len (f :- p)) = f /. (len f) ) A1: len (f :- p) in dom (f :- p) by Th6; assume A2: p in rng f ; ::_thesis: (f :- p) /. (len (f :- p)) = f /. (len f) then p .. f <= len f by FINSEQ_4:21; then reconsider j = (len f) - (p .. f) as Element of NAT by INT_1:5; len (f :- p) = j + 1 by A2, Th50; hence (f :- p) /. (len (f :- p)) = f /. (j + (p .. f)) by A2, A1, Th52 .= f /. (len f) ; ::_thesis: verum end; theorem :: FINSEQ_5:55 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds rng (f :- p) c= rng f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds rng (f :- p) c= rng f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds rng (f :- p) c= rng f let f be FinSequence of D; ::_thesis: ( p in rng f implies rng (f :- p) c= rng f ) assume p in rng f ; ::_thesis: rng (f :- p) c= rng f then ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) by Th49; hence rng (f :- p) c= rng f by Th33; ::_thesis: verum end; theorem :: FINSEQ_5:56 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & f is one-to-one holds f :- p is one-to-one proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & f is one-to-one holds f :- p is one-to-one let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & f is one-to-one holds f :- p is one-to-one let f be FinSequence of D; ::_thesis: ( p in rng f & f is one-to-one implies f :- p is one-to-one ) assume p in rng f ; ::_thesis: ( not f is one-to-one or f :- p is one-to-one ) then ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) by Th49; hence ( not f is one-to-one or f :- p is one-to-one ) ; ::_thesis: verum end; definition let f be FinSequence; func Rev f -> FinSequence means :Def3: :: FINSEQ_5:def 3 ( len it = len f & ( for i being Nat st i in dom it holds it . i = f . (((len f) - i) + 1) ) ); existence ex b1 being FinSequence st ( len b1 = len f & ( for i being Nat st i in dom b1 holds b1 . i = f . (((len f) - i) + 1) ) ) proof deffunc H1( Nat) -> set = f . (((len f) - \$1) + 1); ex p being FinSequence st ( len p = len f & ( for k being Nat st k in dom p holds p . k = H1(k) ) ) from FINSEQ_1:sch_2(); hence ex b1 being FinSequence st ( len b1 = len f & ( for i being Nat st i in dom b1 holds b1 . i = f . (((len f) - i) + 1) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence st len b1 = len f & ( for i being Nat st i in dom b1 holds b1 . i = f . (((len f) - i) + 1) ) & len b2 = len f & ( for i being Nat st i in dom b2 holds b2 . i = f . (((len f) - i) + 1) ) holds b1 = b2 proof A1: dom f = Seg (len f) by FINSEQ_1:def_3; let f1, f2 be FinSequence; ::_thesis: ( len f1 = len f & ( for i being Nat st i in dom f1 holds f1 . i = f . (((len f) - i) + 1) ) & len f2 = len f & ( for i being Nat st i in dom f2 holds f2 . i = f . (((len f) - i) + 1) ) implies f1 = f2 ) assume that A2: len f1 = len f and A3: for i being Nat st i in dom f1 holds f1 . i = f . (((len f) - i) + 1) and A4: len f2 = len f and A5: for i being Nat st i in dom f2 holds f2 . i = f . (((len f) - i) + 1) ; ::_thesis: f1 = f2 A6: dom f1 = Seg (len f1) by FINSEQ_1:def_3; A7: dom f2 = Seg (len f2) by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_ f1_._i_=_f2_._i let i be Nat; ::_thesis: ( i in dom f implies f1 . i = f2 . i ) assume A8: i in dom f ; ::_thesis: f1 . i = f2 . i then f1 . i = f . (((len f) - i) + 1) by A2, A3, A6, A1; hence f1 . i = f2 . i by A4, A5, A7, A1, A8; ::_thesis: verum end; hence f1 = f2 by A2, A4, A6, A1, FINSEQ_2:9; ::_thesis: verum end; involutiveness for b1, b2 being FinSequence st len b1 = len b2 & ( for i being Nat st i in dom b1 holds b1 . i = b2 . (((len b2) - i) + 1) ) holds ( len b2 = len b1 & ( for i being Nat st i in dom b2 holds b2 . i = b1 . (((len b1) - i) + 1) ) ) proof let g, f be FinSequence; ::_thesis: ( len g = len f & ( for i being Nat st i in dom g holds g . i = f . (((len f) - i) + 1) ) implies ( len f = len g & ( for i being Nat st i in dom f holds f . i = g . (((len g) - i) + 1) ) ) ) assume that A9: len g = len f and A10: for i being Nat st i in dom g holds g . i = f . (((len f) - i) + 1) ; ::_thesis: ( len f = len g & ( for i being Nat st i in dom f holds f . i = g . (((len g) - i) + 1) ) ) thus len f = len g by A9; ::_thesis: for i being Nat st i in dom f holds f . i = g . (((len g) - i) + 1) let i be Nat; ::_thesis: ( i in dom f implies f . i = g . (((len g) - i) + 1) ) assume A11: i in dom f ; ::_thesis: f . i = g . (((len g) - i) + 1) then i in dom g by A9, FINSEQ_3:29; then i <= len g by FINSEQ_3:25; then reconsider j = (len g) - i as Element of NAT by INT_1:5; i >= 1 by A11, FINSEQ_3:25; then j + i >= j + 1 by XREAL_1:6; then j + 1 <= len g ; then j < len g by NAT_1:13; then ( 1 <= j + 1 & j + 1 <= len g ) by NAT_1:11, NAT_1:13; then A12: j + 1 in dom g by FINSEQ_3:25; thus f . i = f . (((len f) - (j + 1)) + 1) by A9 .= g . (j + 1) by A10, A12 .= g . (((len g) - i) + 1) ; ::_thesis: verum end; end; :: deftheorem Def3 defines Rev FINSEQ_5:def_3_:_ for f, b2 being FinSequence holds ( b2 = Rev f iff ( len b2 = len f & ( for i being Nat st i in dom b2 holds b2 . i = f . (((len f) - i) + 1) ) ) ); theorem Th57: :: FINSEQ_5:57 for f being FinSequence holds ( dom f = dom (Rev f) & rng f = rng (Rev f) ) proof let f be FinSequence; ::_thesis: ( dom f = dom (Rev f) & rng f = rng (Rev f) ) thus A1: dom f = Seg (len f) by FINSEQ_1:def_3 .= Seg (len (Rev f)) by Def3 .= dom (Rev f) by FINSEQ_1:def_3 ; ::_thesis: rng f = rng (Rev f) A2: len f = len (Rev f) by Def3; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: rng (Rev f) c= rng f let x be set ; ::_thesis: ( x in rng f implies x in rng (Rev f) ) assume x in rng f ; ::_thesis: x in rng (Rev f) then consider i being Nat such that A3: i in dom f and A4: f . i = x by FINSEQ_2:10; i <= len f by A3, FINSEQ_3:25; then reconsider j = ((len f) - i) + 1 as Element of NAT by Th1; dom f = Seg (len f) by FINSEQ_1:def_3; then j in Seg (len (Rev f)) by A2, A3, Th2; then A5: j in dom (Rev f) by FINSEQ_1:def_3; then (Rev f) . j = f . (((len f) - j) + 1) by Def3; hence x in rng (Rev f) by A4, A5, FUNCT_1:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Rev f) or x in rng f ) assume x in rng (Rev f) ; ::_thesis: x in rng f then consider i being Nat such that A6: i in dom (Rev f) and A7: (Rev f) . i = x by FINSEQ_2:10; i <= len f by A2, A6, FINSEQ_3:25; then reconsider j = ((len f) - i) + 1 as Element of NAT by Th1; i in Seg (len (Rev f)) by A6, FINSEQ_1:def_3; then j in Seg (len (Rev f)) by A2, Th2; then A8: j in dom (Rev f) by FINSEQ_1:def_3; (Rev f) . i = f . (((len f) - i) + 1) by A6, Def3; hence x in rng f by A1, A7, A8, FUNCT_1:def_3; ::_thesis: verum end; theorem Th58: :: FINSEQ_5:58 for i being Nat for f being FinSequence st i in dom f holds (Rev f) . i = f . (((len f) - i) + 1) proof let i be Nat; ::_thesis: for f being FinSequence st i in dom f holds (Rev f) . i = f . (((len f) - i) + 1) let f be FinSequence; ::_thesis: ( i in dom f implies (Rev f) . i = f . (((len f) - i) + 1) ) dom f = dom (Rev f) by Th57; hence ( i in dom f implies (Rev f) . i = f . (((len f) - i) + 1) ) by Def3; ::_thesis: verum end; theorem Th59: :: FINSEQ_5:59 for f being FinSequence for i, j being Nat st i in dom f & i + j = (len f) + 1 holds j in dom (Rev f) proof let f be FinSequence; ::_thesis: for i, j being Nat st i in dom f & i + j = (len f) + 1 holds j in dom (Rev f) let i, j be Nat; ::_thesis: ( i in dom f & i + j = (len f) + 1 implies j in dom (Rev f) ) assume that A1: i in dom f and A2: i + j = (len f) + 1 ; ::_thesis: j in dom (Rev f) A3: ( dom f = Seg (len f) & dom f = dom (Rev f) ) by Th57, FINSEQ_1:def_3; j = ((len f) - i) + 1 by A2; hence j in dom (Rev f) by A1, A3, Th2; ::_thesis: verum end; registration let f be empty FinSequence; cluster Rev f -> empty ; coherence Rev f is empty proof len {} = 0 ; then len (Rev {}) = 0 by Def3; hence Rev f is empty ; ::_thesis: verum end; end; theorem :: FINSEQ_5:60 for x being set holds Rev <*x*> = <*x*> proof let x be set ; ::_thesis: Rev <*x*> = <*x*> set f = <*x*>; A1: len <*x*> = 1 by FINSEQ_1:39; now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*x*>_holds_ <*x*>_._i_=_<*x*>_._(((len_<*x*>)_-_i)_+_1) let i be Nat; ::_thesis: ( i in dom <*x*> implies <*x*> . i = <*x*> . (((len <*x*>) - i) + 1) ) assume i in dom <*x*> ; ::_thesis: <*x*> . i = <*x*> . (((len <*x*>) - i) + 1) then i in Seg (len <*x*>) by FINSEQ_1:def_3; then i = 1 by A1, FINSEQ_1:2, TARSKI:def_1; hence <*x*> . i = <*x*> . (((len <*x*>) - i) + 1) by FINSEQ_1:39; ::_thesis: verum end; hence Rev <*x*> = <*x*> by Def3; ::_thesis: verum end; theorem :: FINSEQ_5:61 for x1, x2 being set holds Rev <*x1,x2*> = <*x2,x1*> proof let x1, x2 be set ; ::_thesis: Rev <*x1,x2*> = <*x2,x1*> set f = <*x1,x2*>; set g = <*x2,x1*>; A1: len <*x1,x2*> = 2 by FINSEQ_1:44; A2: len <*x2,x1*> = 2 by FINSEQ_1:44; now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*x2,x1*>_holds_ <*x2,x1*>_._i_=_<*x1,x2*>_._(((len_<*x1,x2*>)_-_i)_+_1) let i be Nat; ::_thesis: ( i in dom <*x2,x1*> implies <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1) ) assume i in dom <*x2,x1*> ; ::_thesis: <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1) then A3: i in Seg (len <*x1,x2*>) by A1, A2, FINSEQ_1:def_3; percases ( i = 1 or i = 2 ) by A1, A3, FINSEQ_1:2, TARSKI:def_2; supposeA4: i = 1 ; ::_thesis: <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1) hence <*x2,x1*> . i = x2 by FINSEQ_1:44 .= <*x1,x2*> . (((len <*x1,x2*>) - i) + 1) by A1, A4, FINSEQ_1:44 ; ::_thesis: verum end; supposeA5: i = 2 ; ::_thesis: <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1) hence <*x2,x1*> . i = x1 by FINSEQ_1:44 .= <*x1,x2*> . (((len <*x1,x2*>) - i) + 1) by A1, A5, FINSEQ_1:44 ; ::_thesis: verum end; end; end; hence Rev <*x1,x2*> = <*x2,x1*> by A1, A2, Def3; ::_thesis: verum end; theorem Th62: :: FINSEQ_5:62 for f being FinSequence holds ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 ) proof let f be FinSequence; ::_thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 ) percases ( f is empty or not f is empty ) ; supposeA1: f is empty ; ::_thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 ) then A2: dom (Rev f) = {} ; thus f . 1 = {} by A1 .= (Rev f) . (len f) by A2, FUNCT_1:def_2 ; ::_thesis: f . (len f) = (Rev f) . 1 thus f . (len f) = {} by A1 .= (Rev f) . 1 by A2, FUNCT_1:def_2 ; ::_thesis: verum end; supposeA3: not f is empty ; ::_thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 ) then len f in Seg (len f) by FINSEQ_1:3; then len f in dom f by FINSEQ_1:def_3; hence (Rev f) . (len f) = f . (((len f) - (len f)) + 1) by Th58 .= f . 1 ; ::_thesis: f . (len f) = (Rev f) . 1 len f >= 1 by A3, NAT_1:14; then 1 in dom f by FINSEQ_3:25; hence (Rev f) . 1 = f . (((len f) - 1) + 1) by Th58 .= f . (len f) ; ::_thesis: verum end; end; end; registration let f be one-to-one FinSequence; cluster Rev f -> one-to-one ; coherence Rev f is one-to-one proof set g = Rev f; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (Rev f) or not x2 in dom (Rev f) or not (Rev f) . x1 = (Rev f) . x2 or x1 = x2 ) assume that A1: x1 in dom (Rev f) and A2: x2 in dom (Rev f) and A3: (Rev f) . x1 = (Rev f) . x2 ; ::_thesis: x1 = x2 reconsider i1 = x1, i2 = x2 as Element of NAT by A1, A2; A4: len (Rev f) = len f by Def3; then ( i1 <= len f & i2 <= len f ) by A1, A2, FINSEQ_3:25; then reconsider i19 = ((len f) - i1) + 1, i29 = ((len f) - i2) + 1 as Element of NAT by Th1; A5: f . i19 = (Rev f) . x1 by A1, Def3 .= f . i29 by A2, A3, Def3 ; ( dom (Rev f) = Seg (len (Rev f)) & dom f = Seg (len f) ) by FINSEQ_1:def_3; then ( i19 in dom f & i29 in dom f ) by A1, A2, A4, Th2; then i19 = i29 by A5, FUNCT_1:def_4; hence x1 = x2 ; ::_thesis: verum end; end; theorem Th63: :: FINSEQ_5:63 for f being FinSequence for x being set holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f) proof let f be FinSequence; ::_thesis: for x being set holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f) let x be set ; ::_thesis: Rev (f ^ <*x*>) = <*x*> ^ (Rev f) set n = (len f) + 1; set g = <*x*>; A1: len (<*x*> ^ (Rev f)) = (len <*x*>) + (len (Rev f)) by FINSEQ_1:22 .= 1 + (len (Rev f)) by FINSEQ_1:39 .= (len f) + 1 by Def3 ; A2: len (f ^ <*x*>) = (len f) + 1 by FINSEQ_2:16; then A3: len (Rev (f ^ <*x*>)) = (len f) + 1 by Def3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Rev_(f_^_<*x*>))_holds_ (Rev_(f_^_<*x*>))_._i_=_(<*x*>_^_(Rev_f))_._i let i be Nat; ::_thesis: ( i in dom (Rev (f ^ <*x*>)) implies (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1 ) A4: len <*x*> = 1 by FINSEQ_1:40; assume A5: i in dom (Rev (f ^ <*x*>)) ; ::_thesis: (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1 then A6: 1 <= i by FINSEQ_3:25; A7: i <= (len f) + 1 by A3, A5, FINSEQ_3:25; percases ( i = 1 or i > 1 ) by A6, XXREAL_0:1; supposeA8: i = 1 ; ::_thesis: (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1 Seg (len <*x*>) = dom <*x*> by FINSEQ_1:def_3; then A9: 1 in dom <*x*> by A4; thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - 1) + 1) by A2, A5, A8, Def3 .= x by FINSEQ_1:42 .= <*x*> . 1 by FINSEQ_1:40 .= (<*x*> ^ (Rev f)) . i by A8, A9, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA10: i > 1 ; ::_thesis: (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1 then reconsider j = i - 1 as Element of NAT by NAT_1:20; consider l being Nat such that A11: i = l + 1 by A10, NAT_1:6; reconsider k = (((len f) + 1) - i) + 1 as Element of NAT by A7, Th1; (len f) + 1 < (len f) + i by A10, XREAL_1:8; then ((len f) + 1) - i < ((len f) + i) - i by XREAL_1:9; then k < (len f) + 1 by XREAL_1:6; then A12: k <= len f by NAT_1:13; i - i <= ((len f) + 1) - i by A7, XREAL_1:9; then 0 + 1 <= k by XREAL_1:6; then A13: k in dom f by A12, FINSEQ_3:25; l <> 0 by A10, A11; then A14: 1 <= j by A11, NAT_1:14; j <= ((len f) + 1) - 1 by A7, XREAL_1:9; then A15: j in dom f by A14, FINSEQ_3:25; thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - i) + 1) by A2, A5, Def3 .= f . (((len f) - j) + 1) by A13, FINSEQ_1:def_7 .= (Rev f) . j by A15, Th58 .= (<*x*> ^ (Rev f)) . i by A1, A7, A4, A10, FINSEQ_1:24 ; ::_thesis: verum end; end; end; hence Rev (f ^ <*x*>) = <*x*> ^ (Rev f) by A1, A3, FINSEQ_2:9; ::_thesis: verum end; theorem :: FINSEQ_5:64 for f, g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f) proof let f be FinSequence; ::_thesis: for g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f) defpred S1[ FinSequence] means Rev (f ^ \$1) = (Rev \$1) ^ (Rev f); A1: S1[ {} ] proof set g = {} ; thus Rev (f ^ {}) = Rev f by FINSEQ_1:34 .= (Rev {}) ^ (Rev f) by FINSEQ_1:34 ; ::_thesis: verum end; A2: for g being FinSequence for x being set st S1[g] holds S1[g ^ <*x*>] proof let g be FinSequence; ::_thesis: for x being set st S1[g] holds S1[g ^ <*x*>] let x be set ; ::_thesis: ( S1[g] implies S1[g ^ <*x*>] ) assume A3: S1[g] ; ::_thesis: S1[g ^ <*x*>] thus Rev (f ^ (g ^ <*x*>)) = Rev ((f ^ g) ^ <*x*>) by FINSEQ_1:32 .= <*x*> ^ ((Rev g) ^ (Rev f)) by A3, Th63 .= (<*x*> ^ (Rev g)) ^ (Rev f) by FINSEQ_1:32 .= (Rev (g ^ <*x*>)) ^ (Rev f) by Th63 ; ::_thesis: verum end; thus for g being FinSequence holds S1[g] from FINSEQ_1:sch_3(A1, A2); ::_thesis: verum end; definition let D be set ; let f be FinSequence of D; :: original: Rev redefine func Rev f -> FinSequence of D; coherence Rev f is FinSequence of D proof set n = len f; A1: dom f = Seg (len f) by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Rev_f)_holds_ (Rev_f)_._i_in_D let i be Nat; ::_thesis: ( i in dom (Rev f) implies (Rev f) . i in D ) set j = ((len f) - i) + 1; assume i in dom (Rev f) ; ::_thesis: (Rev f) . i in D then i in Seg (len (Rev f)) by FINSEQ_1:def_3; then A2: i in Seg (len f) by Def3; then ((len f) - i) + 1 in Seg (len f) by Th2; then f . (((len f) - i) + 1) in D by A1, FINSEQ_2:11; hence (Rev f) . i in D by A1, A2, Th58; ::_thesis: verum end; hence Rev f is FinSequence of D by FINSEQ_2:12; ::_thesis: verum end; end; theorem :: FINSEQ_5:65 for D being non empty set for f being FinSequence of D st not f is empty holds ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D st not f is empty holds ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 ) let f be FinSequence of D; ::_thesis: ( not f is empty implies ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 ) ) A1: dom f = dom (Rev f) by Th57; assume A2: not f is empty ; ::_thesis: ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 ) then A3: len f in dom f by Th6; 1 in dom f by A2, Th6; hence f /. 1 = f . 1 by PARTFUN1:def_6 .= (Rev f) . (len f) by Th62 .= (Rev f) /. (len f) by A3, A1, PARTFUN1:def_6 ; ::_thesis: f /. (len f) = (Rev f) /. 1 thus f /. (len f) = f . (len f) by A3, PARTFUN1:def_6 .= (Rev f) . 1 by Th62 .= (Rev f) /. 1 by A2, A1, Th6, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: FINSEQ_5:66 for j being Nat for D being non empty set for f being FinSequence of D for i being Nat st i in dom f & i + j = (len f) + 1 holds f /. i = (Rev f) /. j proof let j be Nat; ::_thesis: for D being non empty set for f being FinSequence of D for i being Nat st i in dom f & i + j = (len f) + 1 holds f /. i = (Rev f) /. j let D be non empty set ; ::_thesis: for f being FinSequence of D for i being Nat st i in dom f & i + j = (len f) + 1 holds f /. i = (Rev f) /. j let f be FinSequence of D; ::_thesis: for i being Nat st i in dom f & i + j = (len f) + 1 holds f /. i = (Rev f) /. j let i be Nat; ::_thesis: ( i in dom f & i + j = (len f) + 1 implies f /. i = (Rev f) /. j ) assume that A1: i in dom f and A2: i + j = (len f) + 1 ; ::_thesis: f /. i = (Rev f) /. j A3: j in dom (Rev f) by A1, A2, Th59; A4: i = ((len f) - j) + 1 by A2; thus f /. i = f . i by A1, PARTFUN1:def_6 .= (Rev f) . j by A4, A3, Def3 .= (Rev f) /. j by A3, PARTFUN1:def_6 ; ::_thesis: verum end; definition let D be non empty set ; let f be FinSequence of D; let p be Element of D; let n be Nat; func Ins (f,n,p) -> FinSequence of D equals :: FINSEQ_5:def 4 ((f | n) ^ <*p*>) ^ (f /^ n); correctness coherence ((f | n) ^ <*p*>) ^ (f /^ n) is FinSequence of D; ; end; :: deftheorem defines Ins FINSEQ_5:def_4_:_ for D being non empty set for f being FinSequence of D for p being Element of D for n being Nat holds Ins (f,n,p) = ((f | n) ^ <*p*>) ^ (f /^ n); theorem :: FINSEQ_5:67 for D being non empty set for p being Element of D for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f let p be Element of D; ::_thesis: for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f let f be FinSequence of D; ::_thesis: Ins (f,0,p) = <*p*> ^ f thus Ins (f,0,p) = <*p*> ^ (f /^ 0) by FINSEQ_1:34 .= <*p*> ^ f by Th28 ; ::_thesis: verum end; theorem Th68: :: FINSEQ_5:68 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D st len f <= n holds Ins (f,n,p) = f ^ <*p*> proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st len f <= n holds Ins (f,n,p) = f ^ <*p*> let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st len f <= n holds Ins (f,n,p) = f ^ <*p*> let p be Element of D; ::_thesis: for f being FinSequence of D st len f <= n holds Ins (f,n,p) = f ^ <*p*> let f be FinSequence of D; ::_thesis: ( len f <= n implies Ins (f,n,p) = f ^ <*p*> ) assume A1: len f <= n ; ::_thesis: Ins (f,n,p) = f ^ <*p*> then f /^ n is empty by Th32; hence Ins (f,n,p) = (f | n) ^ <*p*> by FINSEQ_1:34 .= f ^ <*p*> by A1, FINSEQ_1:58 ; ::_thesis: verum end; theorem :: FINSEQ_5:69 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1 proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1 let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1 let p be Element of D; ::_thesis: for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1 let f be FinSequence of D; ::_thesis: len (Ins (f,n,p)) = (len f) + 1 percases ( n <= len f or len f < n ) ; supposeA1: n <= len f ; ::_thesis: len (Ins (f,n,p)) = (len f) + 1 thus len (Ins (f,n,p)) = (len ((f | n) ^ <*p*>)) + (len (f /^ n)) by FINSEQ_1:22 .= (len ((f | n) ^ <*p*>)) + ((len f) - n) by A1, RFINSEQ:def_1 .= ((len (f | n)) + (len <*p*>)) + ((len f) - n) by FINSEQ_1:22 .= ((len (f | n)) + 1) + ((len f) - n) by FINSEQ_1:39 .= (n + 1) + ((len f) - n) by A1, FINSEQ_1:59 .= (len f) + 1 ; ::_thesis: verum end; suppose len f < n ; ::_thesis: len (Ins (f,n,p)) = (len f) + 1 then Ins (f,n,p) = f ^ <*p*> by Th68; hence len (Ins (f,n,p)) = (len f) + 1 by FINSEQ_2:16; ::_thesis: verum end; end; end; theorem Th70: :: FINSEQ_5:70 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f) proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f) let p be Element of D; ::_thesis: for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f) let f be FinSequence of D; ::_thesis: rng (Ins (f,n,p)) = {p} \/ (rng f) thus rng (Ins (f,n,p)) = (rng ((f | n) ^ <*p*>)) \/ (rng (f /^ n)) by FINSEQ_1:31 .= ((rng (f | n)) \/ (rng <*p*>)) \/ (rng (f /^ n)) by FINSEQ_1:31 .= ((rng (f | n)) \/ (rng (f /^ n))) \/ (rng <*p*>) by XBOOLE_1:4 .= (rng ((f | n) ^ (f /^ n))) \/ (rng <*p*>) by FINSEQ_1:31 .= (rng <*p*>) \/ (rng f) by RFINSEQ:8 .= {p} \/ (rng f) by FINSEQ_1:38 ; ::_thesis: verum end; registration let D be non empty set ; let f be FinSequence of D; let n be Nat; let p be Element of D; cluster Ins (f,n,p) -> non empty ; coherence not Ins (f,n,p) is empty ; end; theorem :: FINSEQ_5:71 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D holds p in rng (Ins (f,n,p)) proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D holds p in rng (Ins (f,n,p)) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds p in rng (Ins (f,n,p)) let p be Element of D; ::_thesis: for f being FinSequence of D holds p in rng (Ins (f,n,p)) let f be FinSequence of D; ::_thesis: p in rng (Ins (f,n,p)) p in {p} by TARSKI:def_1; then p in {p} \/ (rng f) by XBOOLE_0:def_3; hence p in rng (Ins (f,n,p)) by Th70; ::_thesis: verum end; theorem Th72: :: FINSEQ_5:72 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D for i being Nat st i in dom (f | n) holds (Ins (f,n,p)) /. i = f /. i proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D for i being Nat st i in dom (f | n) holds (Ins (f,n,p)) /. i = f /. i let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D for i being Nat st i in dom (f | n) holds (Ins (f,n,p)) /. i = f /. i let p be Element of D; ::_thesis: for f being FinSequence of D for i being Nat st i in dom (f | n) holds (Ins (f,n,p)) /. i = f /. i let f be FinSequence of D; ::_thesis: for i being Nat st i in dom (f | n) holds (Ins (f,n,p)) /. i = f /. i let i be Nat; ::_thesis: ( i in dom (f | n) implies (Ins (f,n,p)) /. i = f /. i ) assume A1: i in dom (f | n) ; ::_thesis: (Ins (f,n,p)) /. i = f /. i thus (Ins (f,n,p)) /. i = ((f | n) ^ (<*p*> ^ (f /^ n))) /. i by FINSEQ_1:32 .= (f | n) /. i by A1, Lm1 .= f /. i by A1, FINSEQ_4:70 ; ::_thesis: verum end; theorem :: FINSEQ_5:73 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D st n <= len f holds (Ins (f,n,p)) /. (n + 1) = p proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st n <= len f holds (Ins (f,n,p)) /. (n + 1) = p let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st n <= len f holds (Ins (f,n,p)) /. (n + 1) = p let p be Element of D; ::_thesis: for f being FinSequence of D st n <= len f holds (Ins (f,n,p)) /. (n + 1) = p let f be FinSequence of D; ::_thesis: ( n <= len f implies (Ins (f,n,p)) /. (n + 1) = p ) A1: 1 <= n + 1 by NAT_1:11; assume n <= len f ; ::_thesis: (Ins (f,n,p)) /. (n + 1) = p then A2: len (f | n) = n by FINSEQ_1:59; then len ((f | n) ^ <*p*>) = n + 1 by FINSEQ_2:16; then n + 1 in dom ((f | n) ^ <*p*>) by A1, FINSEQ_3:25; hence (Ins (f,n,p)) /. (n + 1) = ((f | n) ^ <*p*>) /. (n + 1) by Lm1 .= p by A2, FINSEQ_4:67 ; ::_thesis: verum end; theorem :: FINSEQ_5:74 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D for i being Nat st n + 1 <= i & i <= len f holds (Ins (f,n,p)) /. (i + 1) = f /. i proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D for i being Nat st n + 1 <= i & i <= len f holds (Ins (f,n,p)) /. (i + 1) = f /. i let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D for i being Nat st n + 1 <= i & i <= len f holds (Ins (f,n,p)) /. (i + 1) = f /. i let p be Element of D; ::_thesis: for f being FinSequence of D for i being Nat st n + 1 <= i & i <= len f holds (Ins (f,n,p)) /. (i + 1) = f /. i let f be FinSequence of D; ::_thesis: for i being Nat st n + 1 <= i & i <= len f holds (Ins (f,n,p)) /. (i + 1) = f /. i let i be Nat; ::_thesis: ( n + 1 <= i & i <= len f implies (Ins (f,n,p)) /. (i + 1) = f /. i ) assume that A1: n + 1 <= i and A2: i <= len f ; ::_thesis: (Ins (f,n,p)) /. (i + 1) = f /. i reconsider j = i - (n + 1) as Element of NAT by A1, INT_1:5; n + (j + 1) <= len f by A2; then A3: j + 1 <= (len f) - n by XREAL_1:19; n <= n + 1 by NAT_1:11; then A4: n <= i by A1, XXREAL_0:2; then len (f | n) = n by A2, FINSEQ_1:59, XXREAL_0:2; then A5: len ((f | n) ^ <*p*>) = n + 1 by FINSEQ_2:16; n <= len f by A2, A4, XXREAL_0:2; then ( 1 <= j + 1 & j + 1 <= len (f /^ n) ) by A3, NAT_1:11, RFINSEQ:def_1; then A6: j + 1 in dom (f /^ n) by FINSEQ_3:25; (n + 1) + (j + 1) = i + 1 ; hence (Ins (f,n,p)) /. (i + 1) = (f /^ n) /. (j + 1) by A5, A6, FINSEQ_4:69 .= f /. (n + (j + 1)) by A6, Th27 .= f /. i ; ::_thesis: verum end; theorem :: FINSEQ_5:75 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D st 1 <= n & not f is empty holds (Ins (f,n,p)) /. 1 = f /. 1 proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st 1 <= n & not f is empty holds (Ins (f,n,p)) /. 1 = f /. 1 let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st 1 <= n & not f is empty holds (Ins (f,n,p)) /. 1 = f /. 1 let p be Element of D; ::_thesis: for f being FinSequence of D st 1 <= n & not f is empty holds (Ins (f,n,p)) /. 1 = f /. 1 let f be FinSequence of D; ::_thesis: ( 1 <= n & not f is empty implies (Ins (f,n,p)) /. 1 = f /. 1 ) assume that A1: 1 <= n and A2: not f is empty ; ::_thesis: (Ins (f,n,p)) /. 1 = f /. 1 A3: ( n <= len f implies len (f | n) = n ) by FINSEQ_1:59; 1 <= len f by A2, NAT_1:14; then 1 <= len (f | n) by A1, A3, FINSEQ_1:58; then 1 in dom (f | n) by FINSEQ_3:25; hence (Ins (f,n,p)) /. 1 = f /. 1 by Th72; ::_thesis: verum end; theorem :: FINSEQ_5:76 for n being Nat for D being non empty set for p being Element of D for f being FinSequence of D st f is one-to-one & not p in rng f holds Ins (f,n,p) is one-to-one proof let n be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st f is one-to-one & not p in rng f holds Ins (f,n,p) is one-to-one let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st f is one-to-one & not p in rng f holds Ins (f,n,p) is one-to-one let p be Element of D; ::_thesis: for f being FinSequence of D st f is one-to-one & not p in rng f holds Ins (f,n,p) is one-to-one let f be FinSequence of D; ::_thesis: ( f is one-to-one & not p in rng f implies Ins (f,n,p) is one-to-one ) assume that A1: f is one-to-one and A2: not p in rng f ; ::_thesis: Ins (f,n,p) is one-to-one now__::_thesis:_for_x_being_set_st_x_in_rng_(f_/^_n)_holds_ not_x_in_rng_((f_|_n)_^_<*p*>) let x be set ; ::_thesis: ( x in rng (f /^ n) implies not x in rng ((f | n) ^ <*p*>) ) assume A3: x in rng (f /^ n) ; ::_thesis: not x in rng ((f | n) ^ <*p*>) rng (f /^ n) c= rng f by Th33; then x in rng f by A3; then not x in {p} by A2, TARSKI:def_1; then A4: not x in rng <*p*> by FINSEQ_1:38; rng (f | n) misses rng (f /^ n) by A1, Th34; then not x in rng (f | n) by A3, XBOOLE_0:3; then not x in (rng (f | n)) \/ (rng <*p*>) by A4, XBOOLE_0:def_3; hence not x in rng ((f | n) ^ <*p*>) by FINSEQ_1:31; ::_thesis: verum end; then A5: rng ((f | n) ^ <*p*>) misses rng (f /^ n) by XBOOLE_0:3; now__::_thesis:_for_x_being_set_st_x_in_rng_<*p*>_holds_ not_x_in_rng_(f_|_n) let x be set ; ::_thesis: ( x in rng <*p*> implies not x in rng (f | n) ) assume x in rng <*p*> ; ::_thesis: not x in rng (f | n) then x in {p} by FINSEQ_1:38; then A6: not x in rng f by A2, TARSKI:def_1; rng (f | n) c= rng f by Th19; hence not x in rng (f | n) by A6; ::_thesis: verum end; then ( <*p*> is one-to-one & rng (f | n) misses rng <*p*> ) by FINSEQ_3:93, XBOOLE_0:3; then (f | n) ^ <*p*> is one-to-one by A1, FINSEQ_3:91; hence Ins (f,n,p) is one-to-one by A1, A5, FINSEQ_3:91; ::_thesis: verum end; begin theorem :: FINSEQ_5:77 for D being non empty set for f being FinSequence of D for i1, i2 being Nat st i1 <= i2 holds ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i1, i2 being Nat st i1 <= i2 holds ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 ) let f be FinSequence of D; ::_thesis: for i1, i2 being Nat st i1 <= i2 holds ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 ) let i1, i2 be Nat; ::_thesis: ( i1 <= i2 implies ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 ) ) assume A1: i1 <= i2 ; ::_thesis: ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 ) len (f | i1) <= i1 by Th17; hence (f | i1) | i2 = f | i1 by A1, FINSEQ_1:58, XXREAL_0:2; ::_thesis: (f | i2) | i1 = f | i1 Seg i1 c= Seg i2 by A1, FINSEQ_1:5; hence (f | i2) | i1 = f | i1 by FUNCT_1:51; ::_thesis: verum end; theorem :: FINSEQ_5:78 for D being non empty set for i being Nat holds (<*> D) | i = <*> D ; theorem :: FINSEQ_5:79 for D being non empty set holds Rev (<*> D) = <*> D ; registration cluster non trivial Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like for set ; existence not for b1 being FinSequence holds b1 is trivial proof take <*0,0*> ; ::_thesis: not <*0,0*> is trivial thus not <*0,0*> is trivial ; ::_thesis: verum end; end; theorem :: FINSEQ_5:80 for D being non empty set for f being FinSequence of D for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 proof let D be non empty set ; ::_thesis: for f being FinSequence of D for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 let f be FinSequence of D; ::_thesis: for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 let l1, l2 be Nat; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 percases ( l1 <= l2 or l1 > l2 ) ; supposeA1: l1 <= l2 ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 percases ( l2 <= len f or l2 > len f ) ; supposeA2: l2 <= len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 then A3: l2 - l1 <= (len f) - l1 by XREAL_1:9; A4: l1 <= len (f | l2) by A1, A2, FINSEQ_1:59; then A5: len ((f | l2) /^ l1) = (len (f | l2)) - l1 by RFINSEQ:def_1 .= l2 - l1 by A2, FINSEQ_1:59 .= l2 -' l1 by A1, XREAL_1:233 ; A6: l1 <= len f by A1, A2, XXREAL_0:2; then len (f /^ l1) = (len f) - l1 by RFINSEQ:def_1; then A7: l2 -' l1 <= len (f /^ l1) by A1, A3, XREAL_1:233; A8: for k being Nat st 1 <= k & k <= len ((f | l2) /^ l1) holds ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len ((f | l2) /^ l1) implies ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k ) assume that A9: 1 <= k and A10: k <= len ((f | l2) /^ l1) ; ::_thesis: ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k A11: k in dom ((f | l2) /^ l1) by A9, A10, FINSEQ_3:25; k <= l2 - l1 by A1, A5, A10, XREAL_1:233; then A12: k + l1 <= (l2 - l1) + l1 by XREAL_1:6; k <= len (f /^ l1) by A7, A5, A10, XXREAL_0:2; then A13: k in dom (f /^ l1) by A9, FINSEQ_3:25; k in NAT by ORDINAL1:def_12; then k in Seg (l2 -' l1) by A5, A9, A10; then ((f /^ l1) | (l2 -' l1)) . k = (f /^ l1) . k by FUNCT_1:49 .= f . (k + l1) by A6, A13, RFINSEQ:def_1 .= (f | l2) . (k + l1) by A12, FINSEQ_3:112 .= ((f | l2) /^ l1) . k by A4, A11, RFINSEQ:def_1 ; hence ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k ; ::_thesis: verum end; len ((f /^ l1) | (l2 -' l1)) = l2 -' l1 by A7, FINSEQ_1:59; hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A5, A8, FINSEQ_1:14; ::_thesis: verum end; supposeA14: l2 > len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 A15: len (f /^ l1) = (len f) -' l1 by RFINSEQ:29; f | l2 = f by A14, FINSEQ_1:58; hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A14, A15, FINSEQ_1:58, NAT_D:42; ::_thesis: verum end; end; end; supposeA16: l1 > l2 ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 reconsider l19 = l1, l29 = l2 as Element of NAT by ORDINAL1:def_12; l1 - l1 > l2 - l1 by A16, XREAL_1:9; then l2 -' l1 = 0 by XREAL_0:def_2; then dom ((f /^ l1) | (l2 -' l1)) = (dom (f /^ l1)) /\ ({} NAT) .= {} NAT ; then A17: (f /^ l1) | (l2 -' l1) = <*> D ; percases ( l1 <= len f or l1 > len f ) ; suppose l1 <= len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 then l19 > len (f | l29) by A16, FINSEQ_1:59, XXREAL_0:2; hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A17, Th32; ::_thesis: verum end; supposeA18: l1 > len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 len (f | l29) <= len f by Th16; hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A17, A18, Th32, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; theorem :: FINSEQ_5:81 for D being set for f being FinSequence of D st len f >= 2 holds f | 2 = <*(f /. 1),(f /. 2)*> proof let D be set ; ::_thesis: for f being FinSequence of D st len f >= 2 holds f | 2 = <*(f /. 1),(f /. 2)*> let f be FinSequence of D; ::_thesis: ( len f >= 2 implies f | 2 = <*(f /. 1),(f /. 2)*> ) set d1 = f /. 1; set d2 = f /. 2; assume A1: len f >= 2 ; ::_thesis: f | 2 = <*(f /. 1),(f /. 2)*> then A2: len (f | 2) = 2 by FINSEQ_1:59; not D is empty by A1; then reconsider D = D as non empty set ; reconsider f = f as FinSequence of D ; 2 in dom (f | 2) by A2, FINSEQ_3:25; then A4: f /. 2 = (f | 2) /. 2 by FINSEQ_4:70 .= (f | 2) . 2 by A2, FINSEQ_4:15 ; 1 in dom (f | 2) by A2, FINSEQ_3:25; then f /. 1 = (f | 2) /. 1 by FINSEQ_4:70 .= (f | 2) . 1 by A2, FINSEQ_4:15 ; hence f | 2 = <*(f /. 1),(f /. 2)*> by A2, A4, FINSEQ_1:44; ::_thesis: verum end; theorem Th82: :: FINSEQ_5:82 for k being Nat for D being set for f being FinSequence of D st k + 1 <= len f holds f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> proof let k be Nat; ::_thesis: for D being set for f being FinSequence of D st k + 1 <= len f holds f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> let D be set ; ::_thesis: for f being FinSequence of D st k + 1 <= len f holds f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> let f be FinSequence of D; ::_thesis: ( k + 1 <= len f implies f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> ) A1: 1 <= k + 1 by NAT_1:12; assume k + 1 <= len f ; ::_thesis: f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> then A2: k + 1 in dom f by A1, FINSEQ_3:25; then f | (Seg (k + 1)) = (f | k) ^ <*(f . (k + 1))*> by Th10; hence f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> by A2, PARTFUN1:def_6; ::_thesis: verum end; theorem Th83: :: FINSEQ_5:83 for D being set for p being FinSequence of D for i being Nat st i < len p holds p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> proof let D be set ; ::_thesis: for p being FinSequence of D for i being Nat st i < len p holds p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> let p be FinSequence of D; ::_thesis: for i being Nat st i < len p holds p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> let i be Nat; ::_thesis: ( i < len p implies p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> ) assume i < len p ; ::_thesis: p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> then A1: i + 1 <= len p by NAT_1:13; 1 <= i + 1 by NAT_1:11; then A2: i + 1 in dom p by A1, FINSEQ_3:25; p | (i + 1) = (p | i) ^ <*(p /. (i + 1))*> by A1, Th82; hence p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by A2, PARTFUN1:def_6; ::_thesis: verum end; theorem :: FINSEQ_5:84 for D being non empty set for p being FinSequence of D for n being Nat st 1 <= n & n <= len p holds p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) proof let D be non empty set ; ::_thesis: for p being FinSequence of D for n being Nat st 1 <= n & n <= len p holds p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) let p be FinSequence of D; ::_thesis: for n being Nat st 1 <= n & n <= len p holds p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) let n be Nat; ::_thesis: ( 1 <= n & n <= len p implies p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) ) assume that A1: 1 <= n and A2: n <= len p ; ::_thesis: p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) len p >= (n -' 1) + 1 by A1, A2, XREAL_1:235; then A3: len p > n -' 1 by NAT_1:13; p | n = p | ((n -' 1) + 1) by A1, XREAL_1:235 .= (p | (n -' 1)) ^ <*(p . ((n -' 1) + 1))*> by A3, Th83 .= (p | (n -' 1)) ^ <*(p . n)*> by A1, XREAL_1:235 ; hence p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) by RFINSEQ:8; ::_thesis: verum end;