:: FINSEQ_7 semantic presentation begin theorem :: FINSEQ_7:1 for D being non empty set for f being FinSequence of D for i, j being Nat st 1 <= i & j <= len f & i < j holds f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j being Nat st 1 <= i & j <= len f & i < j holds f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & j <= len f & i < j holds f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) let i, j be Nat; ::_thesis: ( 1 <= i & j <= len f & i < j implies f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) ) assume that A1: 1 <= i and A2: j <= len f and A3: i < j ; ::_thesis: f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) A4: i <= len f by A2, A3, XXREAL_0:2; 1 <= j by A1, A3, XXREAL_0:2; then A5: j in dom f by A2, FINSEQ_3:25; set I = (j -' i) -' 1; i -' i < j -' i by A3, NAT_D:57; then A6: ((j -' i) -' 1) + 1 = j -' i by NAT_1:14, XREAL_1:235; j -' i <= (len f) -' i by A2, NAT_D:42; then A7: ((j -' i) -' 1) + 1 <= len (f /^ i) by A6, RFINSEQ:29; reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12; A8: i < len (f | j) by A2, A3, FINSEQ_1:59; 1 <= ((j -' i) -' 1) + 1 by NAT_1:14; then A9: ((j -' i) -' 1) + 1 in dom (f /^ i) by A7, FINSEQ_3:25; (((j -' i) -' 1) + 1) + i = j by A3, A6, XREAL_1:235; then A10: (f /^ i) /. (((j -' i) -' 1) + 1) = f /. j by A9, FINSEQ_5:27; A11: f /^ i = ((f | j) ^ (f /^ j)) /^ i by RFINSEQ:8 .= ((f | j) /^ i) ^ (f /^ j) by A8, GENEALG1:1 .= ((f /^ i) | (((j -' i) -' 1) + 1)) ^ (f /^ j) by A6, FINSEQ_5:80 .= (((f /^ i) | ((j -' i) -' 1)) ^ <*((f /^ i) /. (((j -' i) -' 1) + 1))*>) ^ (f /^ j) by A7, FINSEQ_5:82 .= (((f /^ i) | ((j -' i) -' 1)) ^ <*(f . j)*>) ^ (f /^ j) by A5, A10, PARTFUN1:def_6 ; f = ((f | (i -' 1)) ^ <*(f . i)*>) ^ (f /^ i) by A1, A4, FINSEQ_5:84 .= ((f | (i -' 1)) ^ <*(f . i)*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f . j)*> ^ (f /^ j))) by A11, FINSEQ_1:32 .= (((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f . j)*> ^ (f /^ j)) by FINSEQ_1:32 .= ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) by FINSEQ_1:32 ; hence f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) ; ::_thesis: verum end; theorem :: FINSEQ_7:2 for i being Nat for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds (g ^ f) . i = (h ^ f) . i proof let i be Nat; ::_thesis: for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds (g ^ f) . i = (h ^ f) . i let f, g, h be FinSequence; ::_thesis: ( len g = len h & len g < i & i <= len (g ^ f) implies (g ^ f) . i = (h ^ f) . i ) assume that A1: len g = len h and A2: len g < i and A3: i <= len (g ^ f) ; ::_thesis: (g ^ f) . i = (h ^ f) . i i <= (len g) + (len f) by A3, FINSEQ_1:22; then A4: i - (len g) <= ((len g) + (len f)) - (len g) by XREAL_1:9; set k = i - (len g); A5: (len g) - (len g) < i - (len g) by A2, XREAL_1:9; then reconsider k = i - (len g) as Element of NAT by INT_1:3; 0 + 1 <= i - (len g) by A5, INT_1:7; then A6: k in dom f by A4, FINSEQ_3:25; (g ^ f) . i = (g ^ f) . (k + (len g)) .= f . k by A6, FINSEQ_1:def_7 .= (h ^ f) . ((len h) + k) by A6, FINSEQ_1:def_7 ; hence (g ^ f) . i = (h ^ f) . i by A1; ::_thesis: verum end; theorem :: FINSEQ_7:3 for i being Nat for f, g being FinSequence st 1 <= i & i <= len f holds f . i = (g ^ f) . ((len g) + i) proof let i be Nat; ::_thesis: for f, g being FinSequence st 1 <= i & i <= len f holds f . i = (g ^ f) . ((len g) + i) let f, g be FinSequence; ::_thesis: ( 1 <= i & i <= len f implies f . i = (g ^ f) . ((len g) + i) ) assume ( 1 <= i & i <= len f ) ; ::_thesis: f . i = (g ^ f) . ((len g) + i) then i in dom f by FINSEQ_3:25; hence f . i = (g ^ f) . ((len g) + i) by FINSEQ_1:def_7; ::_thesis: verum end; theorem :: FINSEQ_7:4 for D being non empty set for f being FinSequence of D for i, n being Nat st i in dom (f /^ n) holds (f /^ n) . i = f . (n + i) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, n being Nat st i in dom (f /^ n) holds (f /^ n) . i = f . (n + i) let f be FinSequence of D; ::_thesis: for i, n being Nat st i in dom (f /^ n) holds (f /^ n) . i = f . (n + i) let i, n be Nat; ::_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) reconsider i = i, n = n as Element of NAT by ORDINAL1:def_12; A2: n + i in dom f by A1, FINSEQ_5:26; ( (f /^ n) /. i = f /. (n + i) & (f /^ n) /. i = (f /^ n) . i ) by A1, FINSEQ_5:27, PARTFUN1:def_6; hence (f /^ n) . i = f . (n + i) by A2, PARTFUN1:def_6; ::_thesis: verum end; Lm1: for j, i being Nat holds (j -' i) -' 1 = (j -' 1) -' i proof let j, i be Nat; ::_thesis: (j -' i) -' 1 = (j -' 1) -' i (j -' i) -' 1 = j -' (i + 1) by NAT_2:30; hence (j -' i) -' 1 = (j -' 1) -' i by NAT_2:30; ::_thesis: verum end; begin notation let D be non empty set ; let f be FinSequence of D; let i be Nat; let p be Element of D; synonym Replace (f,i,p) for D +* (f,i); end; definition let D be non empty set ; let f be FinSequence of D; let i be Nat; let p be Element of D; :: original: Replace redefine func Replace (f,i,p) -> FinSequence of D equals :Def1: :: FINSEQ_7:def 1 ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) if ( 1 <= i & i <= len f ) otherwise f; compatibility for b1 being FinSequence of D holds ( ( 1 <= i & i <= len f implies ( b1 = Replace (i,p,) iff b1 = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b1 = Replace (i,p,) iff b1 = f ) ) ) proof A1: ( ( not 1 <= i or not i <= len f ) implies f +* (i,p) = f ) proof assume ( not 1 <= i or not i <= len f ) ; ::_thesis: f +* (i,p) = f then not i in dom f by FINSEQ_3:25; hence f +* (i,p) = f by FUNCT_7:def_3; ::_thesis: verum end; ( 1 <= i & i <= len f implies f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) proof assume ( 1 <= i & i <= len f ) ; ::_thesis: f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) then i in dom f by FINSEQ_3:25; hence f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) by FUNCT_7:98; ::_thesis: verum end; hence for b1 being FinSequence of D holds ( ( 1 <= i & i <= len f implies ( b1 = Replace (i,p,) iff b1 = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b1 = Replace (i,p,) iff b1 = f ) ) ) by A1; ::_thesis: verum end; correctness coherence Replace (i,p,) is FinSequence of D; consistency for b1 being FinSequence of D holds verum; proof reconsider i = i as Element of NAT by ORDINAL1:def_12; f +* (i,p) is FinSequence of D ; hence ( Replace (i,p,) is FinSequence of D & ( for b1 being FinSequence of D holds verum ) ) ; ::_thesis: verum end; end; :: deftheorem Def1 defines Replace FINSEQ_7:def_1_:_ for D being non empty set for f being FinSequence of D for i being Nat for p being Element of D holds ( ( 1 <= i & i <= len f implies Replace (f,i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) & ( ( not 1 <= i or not i <= len f ) implies Replace (f,i,p) = f ) ); theorem :: FINSEQ_7:5 for D being non empty set for f being FinSequence of D for p being Element of D for i being Nat holds len (Replace (f,i,p)) = len f by FUNCT_7:97; theorem :: FINSEQ_7:6 for D being non empty set for f being FinSequence of D for p being Element of D for i being Nat holds rng (Replace (f,i,p)) c= (rng f) \/ {p} by FUNCT_7:100; theorem :: FINSEQ_7:7 for D being non empty set for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds p in rng (Replace (f,i,p)) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds p in rng (Replace (f,i,p)) let f be FinSequence of D; ::_thesis: for p being Element of D for i being Nat st 1 <= i & i <= len f holds p in rng (Replace (f,i,p)) let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds p in rng (Replace (f,i,p)) let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies p in rng (Replace (f,i,p)) ) assume ( 1 <= i & i <= len f ) ; ::_thesis: p in rng (Replace (f,i,p)) then i in dom f by FINSEQ_3:25; hence p in rng (Replace (f,i,p)) by FUNCT_7:102; ::_thesis: verum end; Lm2: for D being non empty set for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) . i = p proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) . i = p let f be FinSequence of D; ::_thesis: for p being Element of D for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) . i = p let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) . i = p let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies (Replace (f,i,p)) . i = p ) assume ( 1 <= i & i <= len f ) ; ::_thesis: (Replace (f,i,p)) . i = p then i in dom f by FINSEQ_3:25; hence (Replace (f,i,p)) . i = p by FUNCT_7:31; ::_thesis: verum end; theorem :: FINSEQ_7:8 for D being non empty set for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) /. i = p proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) /. i = p let f be FinSequence of D; ::_thesis: for p being Element of D for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) /. i = p let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds (Replace (f,i,p)) /. i = p let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies (Replace (f,i,p)) /. i = p ) assume ( 1 <= i & i <= len f ) ; ::_thesis: (Replace (f,i,p)) /. i = p then i in dom f by FINSEQ_3:25; hence (Replace (f,i,p)) /. i = p by FUNCT_7:36; ::_thesis: verum end; theorem :: FINSEQ_7:9 for D being non empty set for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds for k being Nat st 0 < k & k <= (len f) - i holds (Replace (f,i,p)) . (i + k) = (f /^ i) . k proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D for i being Nat st 1 <= i & i <= len f holds for k being Nat st 0 < k & k <= (len f) - i holds (Replace (f,i,p)) . (i + k) = (f /^ i) . k let f be FinSequence of D; ::_thesis: for p being Element of D for i being Nat st 1 <= i & i <= len f holds for k being Nat st 0 < k & k <= (len f) - i holds (Replace (f,i,p)) . (i + k) = (f /^ i) . k let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds for k being Nat st 0 < k & k <= (len f) - i holds (Replace (f,i,p)) . (i + k) = (f /^ i) . k let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies for k being Nat st 0 < k & k <= (len f) - i holds (Replace (f,i,p)) . (i + k) = (f /^ i) . k ) assume that A1: 1 <= i and A2: i <= len f ; ::_thesis: for k being Nat st 0 < k & k <= (len f) - i holds (Replace (f,i,p)) . (i + k) = (f /^ i) . k i - 1 < i by XREAL_1:146; then A3: i -' 1 < i by A1, XREAL_1:233; A4: len ((f | (i -' 1)) ^ <*p*>) = (len (f | (i -' 1))) + (len <*p*>) by FINSEQ_1:22 .= (i -' 1) + (len <*p*>) by A2, A3, FINSEQ_1:59, XXREAL_0:2 .= (i -' 1) + 1 by FINSEQ_1:39 .= i by A1, XREAL_1:235 ; let k be Nat; ::_thesis: ( 0 < k & k <= (len f) - i implies (Replace (f,i,p)) . (i + k) = (f /^ i) . k ) assume that A5: 0 < k and A6: k <= (len f) - i ; ::_thesis: (Replace (f,i,p)) . (i + k) = (f /^ i) . k A7: 0 + 1 <= k by A5, INT_1:7; len f = len (Replace (f,i,p)) by FUNCT_7:97 .= len (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) by A1, A2, Def1 .= i + (len (f /^ i)) by A4, FINSEQ_1:22 ; then A8: k in dom (f /^ i) by A6, A7, FINSEQ_3:25; (Replace (f,i,p)) . (i + k) = (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) . ((len ((f | (i -' 1)) ^ <*p*>)) + k) by A1, A2, A4, Def1; hence (Replace (f,i,p)) . (i + k) = (f /^ i) . k by A8, FINSEQ_1:def_7; ::_thesis: verum end; theorem Th10: :: FINSEQ_7:10 for D being non empty set for f being FinSequence of D for p being Element of D for k, i being Nat st 1 <= k & k <= len f & k <> i holds (Replace (f,i,p)) /. k = f /. k proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D for k, i being Nat st 1 <= k & k <= len f & k <> i holds (Replace (f,i,p)) /. k = f /. k let f be FinSequence of D; ::_thesis: for p being Element of D for k, i being Nat st 1 <= k & k <= len f & k <> i holds (Replace (f,i,p)) /. k = f /. k let p be Element of D; ::_thesis: for k, i being Nat st 1 <= k & k <= len f & k <> i holds (Replace (f,i,p)) /. k = f /. k let k, i be Nat; ::_thesis: ( 1 <= k & k <= len f & k <> i implies (Replace (f,i,p)) /. k = f /. k ) assume A1: ( 1 <= k & k <= len f & k <> i ) ; ::_thesis: (Replace (f,i,p)) /. k = f /. k reconsider i = i, k = k as Element of NAT by ORDINAL1:def_12; ( k <> i & k in dom f ) by A1, FINSEQ_3:25; hence (Replace (f,i,p)) /. k = f /. k by FUNCT_7:37; ::_thesis: verum end; theorem Th11: :: FINSEQ_7:11 for D being non empty set for f being FinSequence of D for q, p being Element of D for i, j being Nat st 1 <= i & i < j & j <= len f holds Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for q, p being Element of D for i, j being Nat st 1 <= i & i < j & j <= len f holds Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) let f be FinSequence of D; ::_thesis: for q, p being Element of D for i, j being Nat st 1 <= i & i < j & j <= len f holds Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) let q, p be Element of D; ::_thesis: for i, j being Nat st 1 <= i & i < j & j <= len f holds Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) let i, j be Nat; ::_thesis: ( 1 <= i & i < j & j <= len f implies Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) ) assume that A1: 1 <= i and A2: i < j and A3: j <= len f ; ::_thesis: Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) set fp = f | (j -' 1); A4: j -' 1 <= j by NAT_D:35; 1 + i <= j by A2, INT_1:7; then i <= j -' 1 by NAT_D:55; then A5: i <= len (f | (j -' 1)) by A3, A4, FINSEQ_1:59, XXREAL_0:2; set Q = f /^ j; set F = Replace (f,j,q); A6: 1 <= j by A1, A2, XXREAL_0:2; set fj = <*q*>; set P = (f | (j -' 1)) ^ <*q*>; A7: len ((f | (j -' 1)) ^ <*q*>) = (len (f | (j -' 1))) + (len <*q*>) by FINSEQ_1:22 .= (len (f | (j -' 1))) + 1 by FINSEQ_1:39 .= (j -' 1) + 1 by A3, A4, FINSEQ_1:59, XXREAL_0:2 .= j by A1, A2, XREAL_1:235, XXREAL_0:2 ; A8: i -' 1 < j -' 1 by A1, A2, NAT_D:56; then A9: i -' 1 <= len (f | (j -' 1)) by A3, A4, FINSEQ_1:59, XXREAL_0:2; i <= len f by A2, A3, XXREAL_0:2; then i <= len (Replace (f,j,q)) by FUNCT_7:97; then Replace ((Replace (f,j,q)),i,p) = (((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((Replace (f,j,q)) /^ i) by A1, Def1 .= (((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*q*>) ^ (f /^ j)) /^ i) by A3, A6, Def1 .= (((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*q*>) /^ i) ^ (f /^ j)) by A2, A7, GENEALG1:1 .= (((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) /^ i) ^ <*q*>) ^ (f /^ j)) by A5, GENEALG1:1 .= (((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f /^ i) | ((j -' 1) -' i)) ^ <*q*>) ^ (f /^ j)) by FINSEQ_5:80 .= ((((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' 1) -' i)) ^ <*q*>)) ^ (f /^ j) by FINSEQ_1:32 .= (((((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by FINSEQ_1:32 .= (((((((f | (j -' 1)) ^ <*q*>) ^ (f /^ j)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A3, A6, Def1 .= ((((((f | (j -' 1)) ^ <*q*>) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A2, A7, FINSEQ_5:22, NAT_D:44 .= (((((f | (j -' 1)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A9, FINSEQ_5:22 .= ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A8, FINSEQ_5:77 .= ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) by Lm1 ; hence Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) ; ::_thesis: verum end; theorem :: FINSEQ_7:12 for D being non empty set for p, q being Element of D holds Replace (<*p*>,1,q) = <*q*> proof let D be non empty set ; ::_thesis: for p, q being Element of D holds Replace (<*p*>,1,q) = <*q*> let p, q be Element of D; ::_thesis: Replace (<*p*>,1,q) = <*q*> A1: 1 - 1 = 0 ; set g = <*> D; reconsider P = <*p*> ^ (<*> D) as FinSequence of D ; A2: (<*p*> ^ (<*> D)) /^ 1 = <*> D by FINSEQ_6:45; 1 <= len <*p*> by FINSEQ_1:39; hence Replace (<*p*>,1,q) = ((<*p*> | (1 -' 1)) ^ <*q*>) ^ (<*p*> /^ 1) by Def1 .= ((<*p*> | 0) ^ <*q*>) ^ (<*p*> /^ 1) by A1, XREAL_0:def_2 .= <*q*> ^ (<*p*> /^ 1) by FINSEQ_1:34 .= <*q*> ^ (P /^ 1) by FINSEQ_1:34 .= <*q*> by A2, FINSEQ_1:34 ; ::_thesis: verum end; theorem Th13: :: FINSEQ_7:13 for D being non empty set for p1, p2, q being Element of D holds Replace (<*p1,p2*>,1,q) = <*q,p2*> proof let D be non empty set ; ::_thesis: for p1, p2, q being Element of D holds Replace (<*p1,p2*>,1,q) = <*q,p2*> let p1, p2, q be Element of D; ::_thesis: Replace (<*p1,p2*>,1,q) = <*q,p2*> set f = <*p1,p2*>; A1: len <*p1,p2*> = 2 by FINSEQ_1:44; then A2: 2 in dom <*p1,p2*> by FINSEQ_3:25; 1 + 1 = len <*p1,p2*> by FINSEQ_1:44; then A3: <*p1,p2*> /^ 1 = <*(<*p1,p2*> /. 2)*> by FINSEQ_5:30 .= <*(<*p1,p2*> . 2)*> by A2, PARTFUN1:def_6 ; Replace (<*p1,p2*>,1,q) = ((<*p1,p2*> | (1 -' 1)) ^ <*q*>) ^ (<*p1,p2*> /^ 1) by A1, Def1 .= ((<*p1,p2*> | 0) ^ <*q*>) ^ (<*p1,p2*> /^ 1) by XREAL_1:232 .= ({} ^ <*q*>) ^ <*p2*> by A3, FINSEQ_1:44 .= <*q*> ^ <*p2*> by FINSEQ_1:34 ; hence Replace (<*p1,p2*>,1,q) = <*q,p2*> ; ::_thesis: verum end; theorem Th14: :: FINSEQ_7:14 for D being non empty set for p1, p2, q being Element of D holds Replace (<*p1,p2*>,2,q) = <*p1,q*> proof let D be non empty set ; ::_thesis: for p1, p2, q being Element of D holds Replace (<*p1,p2*>,2,q) = <*p1,q*> let p1, p2, q be Element of D; ::_thesis: Replace (<*p1,p2*>,2,q) = <*p1,q*> set f = <*p1,p2*>; A1: 2 -' 1 = (1 + 1) -' 1 .= 1 by NAT_D:34 ; len <*p1,p2*> = 2 by FINSEQ_1:44; then A2: 1 in dom <*p1,p2*> by FINSEQ_3:25; 2 <= len <*p1,p2*> by FINSEQ_1:44; then Replace (<*p1,p2*>,2,q) = ((<*p1,p2*> | (2 -' 1)) ^ <*q*>) ^ (<*p1,p2*> /^ 2) by Def1 .= ((<*p1,p2*> | 1) ^ <*q*>) ^ (<*p1,p2*> /^ (len <*p1,p2*>)) by A1, FINSEQ_1:44 .= ((<*p1,p2*> | 1) ^ <*q*>) ^ {} by RFINSEQ:27 .= (<*(<*p1,p2*> /. 1)*> ^ <*q*>) ^ {} by FINSEQ_5:20 .= <*(<*p1,p2*> /. 1)*> ^ <*q*> by FINSEQ_1:34 .= <*(<*p1,p2*> . 1)*> ^ <*q*> by A2, PARTFUN1:def_6 .= <*p1*> ^ <*q*> by FINSEQ_1:44 ; hence Replace (<*p1,p2*>,2,q) = <*p1,q*> ; ::_thesis: verum end; theorem Th15: :: FINSEQ_7:15 for D being non empty set for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*> proof let D be non empty set ; ::_thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*> let p1, p2, p3, q be Element of D; ::_thesis: Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*> set f = <*p1,p2,p3*>; len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then Replace (<*p1,p2,p3*>,1,q) = ((<*p1,p2,p3*> | (1 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 1) by Def1 .= ((<*p1,p2,p3*> | 0) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 1) by XREAL_1:232 .= <*q*> ^ (<*p1,p2,p3*> /^ 1) by FINSEQ_1:34 .= <*q*> ^ <*p2,p3*> by FINSEQ_6:47 .= (<*q*> ^ <*p2*>) ^ <*p3*> by FINSEQ_1:32 ; hence Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*> ; ::_thesis: verum end; theorem Th16: :: FINSEQ_7:16 for D being non empty set for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*> proof let D be non empty set ; ::_thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*> let p1, p2, p3, q be Element of D; ::_thesis: Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*> set f = <*p1,p2,p3*>; A1: 2 -' 1 = (1 + 1) -' 1 .= 1 by NAT_D:34 ; A2: len <*p1,p2,p3*> = 2 + 1 by FINSEQ_1:45; A3: len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then A4: 3 in dom <*p1,p2,p3*> by FINSEQ_3:25; A5: 1 in dom <*p1,p2,p3*> by A3, FINSEQ_3:25; Replace (<*p1,p2,p3*>,2,q) = ((<*p1,p2,p3*> | (2 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 2) by A3, Def1 .= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*(<*p1,p2,p3*> /. 3)*> by A1, A2, FINSEQ_5:30 .= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*(<*p1,p2,p3*> . 3)*> by A4, PARTFUN1:def_6 .= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*p3*> by FINSEQ_1:45 .= (<*(<*p1,p2,p3*> /. 1)*> ^ <*q*>) ^ <*p3*> by FINSEQ_5:20 .= (<*(<*p1,p2,p3*> . 1)*> ^ <*q*>) ^ <*p3*> by A5, PARTFUN1:def_6 .= (<*p1*> ^ <*q*>) ^ <*p3*> by FINSEQ_1:45 ; hence Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*> ; ::_thesis: verum end; theorem Th17: :: FINSEQ_7:17 for D being non empty set for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*> proof let D be non empty set ; ::_thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*> let p1, p2, p3, q be Element of D; ::_thesis: Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*> set f = <*p1,p2,p3*>; A1: 3 -' 1 = (2 + 1) -' 1 .= 2 by NAT_D:34 ; A2: len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then A3: 1 in dom <*p1,p2,p3*> by FINSEQ_3:25; A4: 2 in dom <*p1,p2,p3*> by A2, FINSEQ_3:25; 3 <= len <*p1,p2,p3*> by FINSEQ_1:45; then Replace (<*p1,p2,p3*>,3,q) = ((<*p1,p2,p3*> | (3 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 3) by Def1 .= ((<*p1,p2,p3*> | 2) ^ <*q*>) ^ (<*p1,p2,p3*> /^ (len <*p1,p2,p3*>)) by A1, FINSEQ_1:45 .= ((<*p1,p2,p3*> | 2) ^ <*q*>) ^ {} by RFINSEQ:27 .= (<*p1,p2,p3*> | 2) ^ <*q*> by FINSEQ_1:34 .= <*(<*p1,p2,p3*> /. 1),(<*p1,p2,p3*> /. 2)*> ^ <*q*> by A2, FINSEQ_5:81 .= (<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> /. 2)*>) ^ <*q*> by A3, PARTFUN1:def_6 .= (<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*> by A4, PARTFUN1:def_6 .= (<*p1*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*> by FINSEQ_1:45 .= (<*p1*> ^ <*p2*>) ^ <*q*> by FINSEQ_1:45 ; hence Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*> ; ::_thesis: verum end; begin registration let f be FinSequence; let i, j be Nat; cluster Swap (f,i,j) -> FinSequence-like ; correctness coherence Swap (f,i,j) is FinSequence-like ; proof dom (Swap (f,i,j)) = dom f by FUNCT_7:99; hence ex n being Nat st dom (Swap (f,i,j)) = Seg n by FINSEQ_1:def_2; :: according to FINSEQ_1:def_2 ::_thesis: verum end; end; definition let D be non empty set ; let f be FinSequence of D; let i, j be Nat; :: original: Swap redefine func Swap (f,i,j) -> FinSequence of D equals :Def2: :: FINSEQ_7:def 2 Replace ((Replace (f,i,(f /. j))),j,(f /. i)) if ( 1 <= i & i <= len f & 1 <= j & j <= len f ) otherwise f; coherence Swap (f,i,j) is FinSequence of D proof rng (Swap (f,i,j)) = rng f by FUNCT_7:103; hence rng (Swap (f,i,j)) c= D by FINSEQ_1:def_4; :: according to FINSEQ_1:def_4 ::_thesis: verum end; compatibility for b1 being FinSequence of D holds ( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( b1 = Swap (f,i,j) iff b1 = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( b1 = Swap (f,i,j) iff b1 = f ) ) ) proof let IT be FinSequence of D; ::_thesis: ( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( IT = Swap (f,i,j) iff IT = f ) ) ) thus ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) ::_thesis: ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( IT = Swap (f,i,j) iff IT = f ) ) proof assume that A1: ( 1 <= i & i <= len f ) and A2: ( 1 <= j & j <= len f ) ; ::_thesis: ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) A3: j in dom f by A2, FINSEQ_3:25; then A4: f /. j = f . j by PARTFUN1:def_6; A5: i in dom f by A1, FINSEQ_3:25; then f /. i = f . i by PARTFUN1:def_6; hence ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) by A5, A3, A4, FUNCT_7:def_12; ::_thesis: verum end; assume ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: ( IT = Swap (f,i,j) iff IT = f ) then ( not i in dom f or not j in dom f ) by FINSEQ_3:25; hence ( IT = Swap (f,i,j) iff IT = f ) by FUNCT_7:def_12; ::_thesis: verum end; correctness consistency for b1 being FinSequence of D holds verum; ; end; :: deftheorem Def2 defines Swap FINSEQ_7:def_2_:_ for D being non empty set for f being FinSequence of D for i, j being Nat holds ( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap (f,i,j) = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies Swap (f,i,j) = f ) ); theorem Th18: :: FINSEQ_7:18 for D being non empty set for f being FinSequence of D for i, j being Nat holds len (Swap (f,i,j)) = len f proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j being Nat holds len (Swap (f,i,j)) = len f let f be FinSequence of D; ::_thesis: for i, j being Nat holds len (Swap (f,i,j)) = len f let i, j be Nat; ::_thesis: len (Swap (f,i,j)) = len f dom (Swap (f,i,j)) = dom f by FUNCT_7:99; hence len (Swap (f,i,j)) = len f by FINSEQ_3:29; ::_thesis: verum end; Lm3: for D being non empty set for f being FinSequence of D for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) let i, j be Nat; ::_thesis: ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) ) assume that A1: 1 <= i and A2: i <= len f and A3: 1 <= j and A4: j <= len f ; ::_thesis: ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) A5: i in dom f by A1, A2, FINSEQ_3:25; set F = Replace (f,i,(f /. j)); A6: i <= len (Replace (f,i,(f /. j))) by A2, FUNCT_7:97; A7: j <= len (Replace (f,i,(f /. j))) by A4, FUNCT_7:97; A8: j in dom f by A3, A4, FINSEQ_3:25; percases ( i = j or i <> j ) ; supposeA9: i = j ; ::_thesis: ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) (Swap (f,i,j)) . i = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . i by A1, A2, A3, A4, Def2 .= f /. i by A1, A6, A9, Lm2 .= f . i by A5, PARTFUN1:def_6 ; hence ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) by A9; ::_thesis: verum end; supposeA10: i <> j ; ::_thesis: ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) A11: (Swap (f,i,j)) . j = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . j by A1, A2, A3, A4, Def2 .= f /. i by A3, A7, Lm2 ; (Swap (f,i,j)) . i = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . i by A1, A2, A3, A4, Def2 .= (Replace (f,i,(f /. j))) . i by A10, FUNCT_7:32 .= f /. j by A1, A2, Lm2 ; hence ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) by A5, A8, A11, PARTFUN1:def_6; ::_thesis: verum end; end; end; theorem Th19: :: FINSEQ_7:19 for D being non empty set for f being FinSequence of D for i being Nat holds Swap (f,i,i) = f proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i being Nat holds Swap (f,i,i) = f let f be FinSequence of D; ::_thesis: for i being Nat holds Swap (f,i,i) = f let i be Nat; ::_thesis: Swap (f,i,i) = f reconsider i = i as Element of NAT by ORDINAL1:def_12; percases ( ( 1 <= i & i <= len f ) or not 1 <= i or not i <= len f ) ; suppose ( 1 <= i & i <= len f ) ; ::_thesis: Swap (f,i,i) = f then Swap (f,i,i) = Replace ((Replace (f,i,(f /. i))),i,(f /. i)) by Def2 .= Replace (f,i,(f /. i)) by FUNCT_7:38 ; hence Swap (f,i,i) = f by FUNCT_7:38; ::_thesis: verum end; suppose ( not 1 <= i or not i <= len f ) ; ::_thesis: Swap (f,i,i) = f hence Swap (f,i,i) = f by Def2; ::_thesis: verum end; end; end; theorem :: FINSEQ_7:20 for D being non empty set for f being FinSequence of D for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f let f be FinSequence of D; ::_thesis: for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f let i, j be Nat; ::_thesis: Swap ((Swap (f,i,j)),j,i) = f percases ( ( 1 <= i & i <= len f & 1 <= j & j <= len f ) or not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; supposeA1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; ::_thesis: Swap ((Swap (f,i,j)),j,i) = f A2: for k being Nat st 1 <= k & k <= len f holds f . k = (Swap ((Swap (f,i,j)),j,i)) . k proof A3: i <= len (Swap (f,i,j)) by A1, Th18; A4: j <= len (Swap (f,i,j)) by A1, Th18; let k be Nat; ::_thesis: ( 1 <= k & k <= len f implies f . k = (Swap ((Swap (f,i,j)),j,i)) . k ) assume that A5: 1 <= k and A6: k <= len f ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k A7: k <= len (Swap (f,i,j)) by A6, Th18; now__::_thesis:_f_._k_=_(Swap_((Swap_(f,i,j)),j,i))_._k percases ( i = k or i <> k ) ; suppose i = k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k then (Swap ((Swap (f,i,j)),j,i)) . k = (Swap (f,k,j)) . j by A1, A7, A4, Lm3; hence f . k = (Swap ((Swap (f,i,j)),j,i)) . k by A1, A5, A6, Lm3; ::_thesis: verum end; supposeA8: i <> k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k now__::_thesis:_f_._k_=_(Swap_((Swap_(f,i,j)),j,i))_._k percases ( j = k or j <> k ) ; suppose j = k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k then (Swap ((Swap (f,i,j)),j,i)) . k = (Swap (f,i,k)) . i by A1, A7, A3, Lm3; hence f . k = (Swap ((Swap (f,i,j)),j,i)) . k by A1, A5, A6, Lm3; ::_thesis: verum end; supposeA9: j <> k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k set S = Swap (f,i,j); (Swap ((Swap (f,i,j)),j,i)) . k = (Replace ((Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. i))),i,((Swap (f,i,j)) /. j))) . k by A1, A4, A3, Def2 .= (Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. i))) . k by A8, FUNCT_7:32 .= (Swap (f,i,j)) . k by A9, FUNCT_7:32 .= (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k by A1, Def2 .= (Replace (f,i,(f /. j))) . k by A9, FUNCT_7:32 ; hence f . k = (Swap ((Swap (f,i,j)),j,i)) . k by A8, FUNCT_7:32; ::_thesis: verum end; end; end; hence f . k = (Swap ((Swap (f,i,j)),j,i)) . k ; ::_thesis: verum end; end; end; hence f . k = (Swap ((Swap (f,i,j)),j,i)) . k ; ::_thesis: verum end; len (Swap ((Swap (f,i,j)),j,i)) = len (Swap (f,i,j)) by Th18 .= len f by Th18 ; hence Swap ((Swap (f,i,j)),j,i) = f by A2, FINSEQ_1:14; ::_thesis: verum end; supposeA10: ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: Swap ((Swap (f,i,j)),j,i) = f then Swap ((Swap (f,i,j)),j,i) = Swap (f,j,i) by Def2; hence Swap ((Swap (f,i,j)),j,i) = f by A10, Def2; ::_thesis: verum end; end; end; theorem Th21: :: FINSEQ_7:21 for D being non empty set for f being FinSequence of D for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i) let f be FinSequence of D; ::_thesis: for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i) let i, j be Nat; ::_thesis: Swap (f,i,j) = Swap (f,j,i) percases ( ( 1 <= i & i <= len f & 1 <= j & j <= len f ) or not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; supposeA1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; ::_thesis: Swap (f,i,j) = Swap (f,j,i) set FJ = Replace (f,j,(f /. i)); set FI = Replace (f,i,(f /. j)); A2: for k being Nat st 1 <= k & k <= len (Swap (f,i,j)) holds (Swap (f,i,j)) . k = (Swap (f,j,i)) . k proof A3: len (Swap (f,i,j)) = len f by Th18 .= len (Replace (f,j,(f /. i))) by FUNCT_7:97 ; A4: len (Swap (f,i,j)) = len f by Th18 .= len (Replace (f,i,(f /. j))) by FUNCT_7:97 ; let k be Nat; ::_thesis: ( 1 <= k & k <= len (Swap (f,i,j)) implies (Swap (f,i,j)) . k = (Swap (f,j,i)) . k ) assume that A5: 1 <= k and A6: k <= len (Swap (f,i,j)) ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k A7: k <= len f by A6, Th18; now__::_thesis:_(Swap_(f,i,j))_._k_=_(Swap_(f,j,i))_._k percases ( i = k or i <> k ) ; supposeA8: i = k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k now__::_thesis:_(Swap_(f,i,j))_._k_=_(Swap_(f,j,i))_._k percases ( j = k or j <> k ) ; supposeA9: j = k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k then (Swap (f,i,k)) . k = (Replace ((Replace (f,i,(f /. j))),k,(f /. i))) . k by A1, Def2 .= f /. i by A5, A6, A4, Lm2 .= (Replace ((Replace (f,j,(f /. i))),k,(f /. i))) . k by A5, A6, A3, Lm2 .= (Swap (f,k,i)) . k by A1, A8, A9, Def2 ; hence (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A9; ::_thesis: verum end; supposeA10: j <> k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k (Swap (f,i,j)) . k = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k by A1, Def2 .= (Replace (f,k,(f /. j))) . k by A8, A10, FUNCT_7:32 .= f /. j by A5, A7, Lm2 .= (Replace ((Replace (f,j,(f /. i))),k,(f /. j))) . k by A5, A6, A3, Lm2 ; hence (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A1, A8, Def2; ::_thesis: verum end; end; end; hence (Swap (f,i,j)) . k = (Swap (f,j,i)) . k ; ::_thesis: verum end; supposeA11: i <> k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k now__::_thesis:_(Swap_(f,i,j))_._k_=_(Swap_(f,j,i))_._k percases ( j = k or j <> k ) ; supposeA12: j = k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k then (Swap (f,i,j)) . k = (Replace ((Replace (f,i,(f /. j))),k,(f /. i))) . k by A1, Def2 .= f /. i by A5, A6, A4, Lm2 .= (Replace (f,j,(f /. i))) . k by A5, A7, A12, Lm2 .= (Replace ((Replace (f,j,(f /. i))),i,(f /. j))) . k by A11, FUNCT_7:32 ; hence (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A1, Def2; ::_thesis: verum end; supposeA13: j <> k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k (Swap (f,i,j)) . k = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k by A1, Def2 .= (Replace (f,i,(f /. j))) . k by A13, FUNCT_7:32 .= f . k by A11, FUNCT_7:32 .= (Replace (f,j,(f /. i))) . k by A13, FUNCT_7:32 .= (Replace ((Replace (f,j,(f /. i))),i,(f /. j))) . k by A11, FUNCT_7:32 ; hence (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A1, Def2; ::_thesis: verum end; end; end; hence (Swap (f,i,j)) . k = (Swap (f,j,i)) . k ; ::_thesis: verum end; end; end; hence (Swap (f,i,j)) . k = (Swap (f,j,i)) . k ; ::_thesis: verum end; len (Swap (f,i,j)) = len f by Th18 .= len (Swap (f,j,i)) by Th18 ; hence Swap (f,i,j) = Swap (f,j,i) by A2, FINSEQ_1:14; ::_thesis: verum end; supposeA14: ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: Swap (f,i,j) = Swap (f,j,i) then Swap (f,i,j) = f by Def2; hence Swap (f,i,j) = Swap (f,j,i) by A14, Def2; ::_thesis: verum end; end; end; theorem :: FINSEQ_7:22 for D being non empty set for f being FinSequence of D for i, j being Nat holds rng (Swap (f,i,j)) = rng f by FUNCT_7:103; theorem :: FINSEQ_7:23 for D being non empty set for p1, p2 being Element of D holds Swap (<*p1,p2*>,1,2) = <*p2,p1*> proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D holds Swap (<*p1,p2*>,1,2) = <*p2,p1*> let p1, p2 be Element of D; ::_thesis: Swap (<*p1,p2*>,1,2) = <*p2,p1*> set f = <*p1,p2*>; A1: len <*p1,p2*> = 2 by FINSEQ_1:44; then 1 in dom <*p1,p2*> by FINSEQ_3:25; then A2: <*p1,p2*> /. 1 = <*p1,p2*> . 1 by PARTFUN1:def_6 .= p1 by FINSEQ_1:44 ; 2 in dom <*p1,p2*> by A1, FINSEQ_3:25; then A3: <*p1,p2*> /. 2 = <*p1,p2*> . 2 by PARTFUN1:def_6 .= p2 by FINSEQ_1:44 ; Swap (<*p1,p2*>,1,2) = Replace ((Replace (<*p1,p2*>,1,(<*p1,p2*> /. 2))),2,(<*p1,p2*> /. 1)) by A1, Def2 .= Replace (<*p2,p2*>,2,(<*p1,p2*> /. 1)) by A3, Th13 ; hence Swap (<*p1,p2*>,1,2) = <*p2,p1*> by A2, Th14; ::_thesis: verum end; theorem :: FINSEQ_7:24 for D being non empty set for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*> let p1, p2, p3 be Element of D; ::_thesis: Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*> set f = <*p1,p2,p3*>; A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then 1 in dom <*p1,p2,p3*> by FINSEQ_3:25; then A2: <*p1,p2,p3*> /. 1 = <*p1,p2,p3*> . 1 by PARTFUN1:def_6 .= p1 by FINSEQ_1:45 ; 2 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25; then A3: <*p1,p2,p3*> /. 2 = <*p1,p2,p3*> . 2 by PARTFUN1:def_6 .= p2 by FINSEQ_1:45 ; Swap (<*p1,p2,p3*>,1,2) = Replace ((Replace (<*p1,p2,p3*>,1,(<*p1,p2,p3*> /. 2))),2,(<*p1,p2,p3*> /. 1)) by A1, Def2 .= Replace (<*p2,p2,p3*>,2,(<*p1,p2,p3*> /. 1)) by A3, Th15 ; hence Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*> by A2, Th16; ::_thesis: verum end; theorem :: FINSEQ_7:25 for D being non empty set for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*> let p1, p2, p3 be Element of D; ::_thesis: Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*> set f = <*p1,p2,p3*>; A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then 1 in dom <*p1,p2,p3*> by FINSEQ_3:25; then A2: <*p1,p2,p3*> /. 1 = <*p1,p2,p3*> . 1 by PARTFUN1:def_6 .= p1 by FINSEQ_1:45 ; 3 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25; then A3: <*p1,p2,p3*> /. 3 = <*p1,p2,p3*> . 3 by PARTFUN1:def_6 .= p3 by FINSEQ_1:45 ; Swap (<*p1,p2,p3*>,1,3) = Replace ((Replace (<*p1,p2,p3*>,1,(<*p1,p2,p3*> /. 3))),3,(<*p1,p2,p3*> /. 1)) by A1, Def2 .= Replace (<*p3,p2,p3*>,3,(<*p1,p2,p3*> /. 1)) by A3, Th15 ; hence Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*> by A2, Th17; ::_thesis: verum end; theorem :: FINSEQ_7:26 for D being non empty set for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*> let p1, p2, p3 be Element of D; ::_thesis: Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*> set f = <*p1,p2,p3*>; A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then 2 in dom <*p1,p2,p3*> by FINSEQ_3:25; then A2: <*p1,p2,p3*> /. 2 = <*p1,p2,p3*> . 2 by PARTFUN1:def_6 .= p2 by FINSEQ_1:45 ; 3 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25; then A3: <*p1,p2,p3*> /. 3 = <*p1,p2,p3*> . 3 by PARTFUN1:def_6 .= p3 by FINSEQ_1:45 ; Swap (<*p1,p2,p3*>,2,3) = Replace ((Replace (<*p1,p2,p3*>,2,(<*p1,p2,p3*> /. 3))),3,(<*p1,p2,p3*> /. 2)) by A1, Def2 .= Replace (<*p1,p3,p3*>,3,(<*p1,p2,p3*> /. 2)) by A3, Th16 ; hence Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*> by A2, Th17; ::_thesis: verum end; theorem Th27: :: FINSEQ_7:27 for D being non empty set for f being FinSequence of D for i, j being Nat st 1 <= i & i < j & j <= len f holds Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j being Nat st 1 <= i & i < j & j <= len f holds Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & i < j & j <= len f holds Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) let i, j be Nat; ::_thesis: ( 1 <= i & i < j & j <= len f implies Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) ) assume that A1: 1 <= i and A2: i < j and A3: j <= len f ; ::_thesis: Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) A4: ( i <= len f & 1 <= j ) by A1, A2, A3, XXREAL_0:2; Swap (f,i,j) = Swap (f,j,i) by Th21 .= Replace ((Replace (f,j,(f /. i))),i,(f /. j)) by A1, A3, A4, Def2 ; hence Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) by A1, A2, A3, Th11; ::_thesis: verum end; theorem :: FINSEQ_7:28 for D being non empty set for f being FinSequence of D for i being Nat st 1 < i & i <= len f holds Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i being Nat st 1 < i & i <= len f holds Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) let f be FinSequence of D; ::_thesis: for i being Nat st 1 < i & i <= len f holds Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) let i be Nat; ::_thesis: ( 1 < i & i <= len f implies Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) ) assume ( 1 < i & i <= len f ) ; ::_thesis: Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) then Swap (f,1,i) = ((((f | (1 -' 1)) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by Th27 .= ((((f | 0) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by XREAL_1:232 .= ((<*(f /. i)*> ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by FINSEQ_1:34 ; hence Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) by NAT_D:45; ::_thesis: verum end; theorem :: FINSEQ_7:29 for D being non empty set for f being FinSequence of D for i being Nat st 1 <= i & i < len f holds Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i being Nat st 1 <= i & i < len f holds Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> let f be FinSequence of D; ::_thesis: for i being Nat st 1 <= i & i < len f holds Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> let i be Nat; ::_thesis: ( 1 <= i & i < len f implies Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> ) assume ( 1 <= i & i < len f ) ; ::_thesis: Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> then Swap (f,i,(len f)) = ((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ (len f)) by Th27 .= ((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ {} by RFINSEQ:27 ; hence Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> by FINSEQ_1:34; ::_thesis: verum end; Lm4: for D being non empty set for f being FinSequence of D for i, k, j being Nat st i <> k & j <> k holds (Swap (f,i,j)) . k = f . k proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, k, j being Nat st i <> k & j <> k holds (Swap (f,i,j)) . k = f . k let f be FinSequence of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k holds (Swap (f,i,j)) . k = f . k let i, k, j be Nat; ::_thesis: ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k ) percases ( ( 1 <= i & i <= len f & 1 <= j & j <= len f ) or not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; supposeA1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; ::_thesis: ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k ) assume that A2: i <> k and A3: j <> k ; ::_thesis: (Swap (f,i,j)) . k = f . k (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k = (Replace (f,i,(f /. j))) . k by A3, FUNCT_7:32 .= f . k by A2, FUNCT_7:32 ; hence (Swap (f,i,j)) . k = f . k by A1, Def2; ::_thesis: verum end; suppose ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k ) hence ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k ) by Def2; ::_thesis: verum end; end; end; theorem Th30: :: FINSEQ_7:30 for D being non empty set for f being FinSequence of D for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds (Swap (f,i,j)) /. k = f /. k proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds (Swap (f,i,j)) /. k = f /. k let f be FinSequence of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds (Swap (f,i,j)) /. k = f /. k let i, k, j be Nat; ::_thesis: ( i <> k & j <> k & 1 <= k & k <= len f implies (Swap (f,i,j)) /. k = f /. k ) assume that A1: ( i <> k & j <> k ) and A2: 1 <= k and A3: k <= len f ; ::_thesis: (Swap (f,i,j)) /. k = f /. k A4: k in dom f by A2, A3, FINSEQ_3:25; k <= len (Swap (f,i,j)) by A3, Th18; then k in dom (Swap (f,i,j)) by A2, FINSEQ_3:25; hence (Swap (f,i,j)) /. k = (Swap (f,i,j)) . k by PARTFUN1:def_6 .= f . k by A1, Lm4 .= f /. k by A4, PARTFUN1:def_6 ; ::_thesis: verum end; theorem Th31: :: FINSEQ_7:31 for D being non empty set for f being FinSequence of D for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) let i, j be Nat; ::_thesis: ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) ) assume that A1: 1 <= i and A2: i <= len f and A3: 1 <= j and A4: j <= len f ; ::_thesis: ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) A5: i in dom f by A1, A2, FINSEQ_3:25; set F = Swap (f,i,j); j <= len (Swap (f,i,j)) by A4, Th18; then j in dom (Swap (f,i,j)) by A3, FINSEQ_3:25; then A6: (Swap (f,i,j)) /. j = (Swap (f,i,j)) . j by PARTFUN1:def_6 .= f . i by A1, A2, A3, A4, Lm3 .= f /. i by A5, PARTFUN1:def_6 ; A7: j in dom f by A3, A4, FINSEQ_3:25; i <= len (Swap (f,i,j)) by A2, Th18; then i in dom (Swap (f,i,j)) by A1, FINSEQ_3:25; then (Swap (f,i,j)) /. i = (Swap (f,i,j)) . i by PARTFUN1:def_6 .= f . j by A1, A2, A3, A4, Lm3 .= f /. j by A7, PARTFUN1:def_6 ; hence ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) by A6; ::_thesis: verum end; begin theorem Th32: :: FINSEQ_7:32 for D being non empty set for f being FinSequence of D for p being Element of D for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) let f be FinSequence of D; ::_thesis: for p being Element of D for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) let p be Element of D; ::_thesis: for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) let i, j be Nat; ::_thesis: ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) ) assume that A1: 1 <= i and A2: i <= len f and A3: 1 <= j and A4: j <= len f ; ::_thesis: Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) A5: i in dom f by A1, A2, FINSEQ_3:25; percases ( i = j or i < j or i > j ) by XXREAL_0:1; supposeA6: i = j ; ::_thesis: Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) then Replace ((Swap (f,i,j)),i,p) = Replace (f,i,p) by Th19; hence Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) by A6, Th19; ::_thesis: verum end; supposeA7: i < j ; ::_thesis: Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) set N = <*(f /. j)*>; set M = f | (i -' 1); set F = Swap (f,i,j); set P = (f | (i -' 1)) ^ <*(f /. j)*>; A8: Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) by A1, A4, A7, Th27 .= (((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f /. i)*> ^ (f /^ j)) by FINSEQ_1:32 .= ((f | (i -' 1)) ^ <*(f /. j)*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))) by FINSEQ_1:32 ; set F1 = Replace (f,j,p); i <= len (Replace (f,j,p)) by A2, FUNCT_7:97; then A9: i in dom (Replace (f,j,p)) by A1, FINSEQ_3:25; A10: f . i = (Replace (f,j,p)) . i by A7, FUNCT_7:32 .= (Replace (f,j,p)) /. i by A9, PARTFUN1:def_6 ; A11: j <= len (Replace (f,j,p)) by A4, FUNCT_7:97; then A12: j in dom (Replace (f,j,p)) by A3, FINSEQ_3:25; set G1 = f | (j -' 1); A13: j -' 1 <= j by NAT_D:35; A14: i -' 1 < j -' 1 by A1, A7, NAT_D:56; then A15: i -' 1 <= len (f | (j -' 1)) by A4, A13, FINSEQ_1:59, XXREAL_0:2; set H1 = <*p*>; set Q = ((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)); A16: i -' 1 <= i by NAT_D:35; A17: i <= len (Swap (f,i,j)) by A2, Th18; len ((f | (i -' 1)) ^ <*(f /. j)*>) = (len (f | (i -' 1))) + (len <*(f /. j)*>) by FINSEQ_1:22 .= (len (f | (i -' 1))) + 1 by FINSEQ_1:39 .= (i -' 1) + 1 by A2, A16, FINSEQ_1:59, XXREAL_0:2 .= i by A1, XREAL_1:235 ; then A18: Replace ((Swap (f,i,j)),i,p) = (((Swap (f,i,j)) | (i -' 1)) ^ <*p*>) ^ ((Swap (f,i,j)) /^ (len ((f | (i -' 1)) ^ <*(f /. j)*>))) by A1, A17, Def1 .= (((Swap (f,i,j)) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))) by A8, FINSEQ_5:37 .= ((((f | (i -' 1)) ^ (<*(f /. j)*> ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))))) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))) by A8, FINSEQ_1:32 .= ((((f | (i -' 1)) ^ (<*(f /. j)*> ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))))) | (len (f | (i -' 1)))) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))) by A2, A16, FINSEQ_1:59, XXREAL_0:2 .= ((f | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))) by FINSEQ_5:23 ; A19: len ((f | (j -' 1)) ^ <*p*>) = (len (f | (j -' 1))) + (len <*p*>) by FINSEQ_1:22 .= (len (f | (j -' 1))) + 1 by FINSEQ_1:39 .= (j -' 1) + 1 by A4, A13, FINSEQ_1:59, XXREAL_0:2 .= j by A3, XREAL_1:235 ; A20: ((Replace (f,j,p)) /^ i) | ((j -' i) -' 1) = ((Replace (f,j,p)) /^ i) | (j -' (i + 1)) by NAT_2:30 .= ((Replace (f,j,p)) /^ i) | ((j -' 1) -' i) by NAT_2:30 .= ((Replace (f,j,p)) | (j -' 1)) /^ i by FINSEQ_5:80 .= ((((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j -' 1)) /^ i by A3, A4, Def1 .= (((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (j -' 1)) /^ i by FINSEQ_1:32 .= (((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (len (f | (j -' 1)))) /^ i by A4, A13, FINSEQ_1:59, XXREAL_0:2 .= (f | (j -' 1)) /^ i by FINSEQ_5:23 .= (f /^ i) | ((j -' 1) -' i) by FINSEQ_5:80 .= (f /^ i) | (j -' (1 + i)) by NAT_2:30 .= (f /^ i) | ((j -' i) -' 1) by NAT_2:30 ; A21: p = (Replace (f,j,p)) . j by A3, A4, Lm2 .= (Replace (f,j,p)) /. j by A12, PARTFUN1:def_6 ; A22: (Replace (f,j,p)) | (i -' 1) = (((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (i -' 1) by A3, A4, Def1 .= ((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (i -' 1) by FINSEQ_1:32 .= (f | (j -' 1)) | (i -' 1) by A15, FINSEQ_5:22 .= f | (i -' 1) by A14, FINSEQ_5:77 ; A23: (Replace (f,j,p)) /^ j = (((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) /^ j by A3, A4, Def1 .= f /^ j by A19, FINSEQ_5:37 ; Swap ((Replace (f,j,p)),i,j) = (((((Replace (f,j,p)) | (i -' 1)) ^ <*((Replace (f,j,p)) /. j)*>) ^ (((Replace (f,j,p)) /^ i) | ((j -' i) -' 1))) ^ <*((Replace (f,j,p)) /. i)*>) ^ ((Replace (f,j,p)) /^ j) by A1, A7, A11, Th27 .= (((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f . i)*> ^ (f /^ j)) by A23, A22, A20, A10, A21, FINSEQ_1:32 .= (((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f /. i)*> ^ (f /^ j)) by A5, PARTFUN1:def_6 .= ((f | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))) by FINSEQ_1:32 ; hence Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) by A18; ::_thesis: verum end; supposeA24: i > j ; ::_thesis: Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) then consider k being Nat such that A25: i = j + k by NAT_1:10; reconsider i = i, j = j, k = k as Element of NAT by ORDINAL1:def_12; A26: i - j > j - j by A24, XREAL_1:9; then A27: k = i -' j by A25, XREAL_0:def_2; set X = f /^ i; set W = <*(f /. j)*>; set V = (f /^ j) | ((i -' j) -' 1); set N = <*(f /. i)*>; set M = f | (j -' 1); set F = Swap (f,j,i); set P = (f | (j -' 1)) ^ <*(f /. i)*>; A28: Swap (f,j,i) = ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>) ^ (f /^ i) by A2, A3, A24, Th27 .= (((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ (<*(f /. j)*> ^ (f /^ i)) by FINSEQ_1:32 .= ((f | (j -' 1)) ^ <*(f /. i)*>) ^ (((f /^ j) | ((i -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ i))) by FINSEQ_1:32 .= ((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)) by FINSEQ_1:32 ; A29: j - 1 >= 1 - 1 by A3, XREAL_1:9; A30: (k + j) -' 1 = (k + j) - 1 by A25, A26, NAT_1:14, NAT_D:37 .= k + (j - 1) .= k + (j -' 1) by A29, XREAL_0:def_2 ; A31: k = 1 + (k -' 1) by A25, A26, NAT_1:14, XREAL_1:235; set Q = (((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i); A32: j -' 1 <= j by NAT_D:35; set F1 = Replace (f,j,p); set G1 = f | (j -' 1); A33: j -' 1 <= j by NAT_D:35; set H1 = <*p*>; j <= len (Replace (f,j,p)) by A4, FUNCT_7:97; then A34: j in dom (Replace (f,j,p)) by A3, FINSEQ_3:25; A35: len ((f | (j -' 1)) ^ <*p*>) = (len (f | (j -' 1))) + (len <*p*>) by FINSEQ_1:22 .= (len (f | (j -' 1))) + 1 by FINSEQ_1:39 .= (j -' 1) + 1 by A4, A33, FINSEQ_1:59, XXREAL_0:2 .= j by A3, XREAL_1:235 ; then A36: (Replace (f,j,p)) /^ i = (((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) /^ ((len ((f | (j -' 1)) ^ <*p*>)) + k) by A3, A4, A25, Def1 .= (f /^ j) /^ k by FINSEQ_5:36 .= f /^ i by A25, FINSEQ_6:81 ; k >= 1 by A25, A26, NAT_1:14; then A37: k - 1 >= 1 - 1 by XREAL_1:9; A38: (j + k) -' 1 = (j + k) - 1 by A3, NAT_D:37 .= j + (k - 1) .= j + (k -' 1) by A37, XREAL_0:def_2 ; A39: i <= len (Replace (f,j,p)) by A2, FUNCT_7:97; then A40: i in dom (Replace (f,j,p)) by A1, FINSEQ_3:25; A41: ((Replace (f,j,p)) /^ j) | ((i -' j) -' 1) = ((Replace (f,j,p)) /^ j) | (i -' (j + 1)) by NAT_2:30 .= ((Replace (f,j,p)) /^ j) | ((i -' 1) -' j) by NAT_2:30 .= ((Replace (f,j,p)) | (i -' 1)) /^ j by FINSEQ_5:80 .= ((((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j + (k -' 1))) /^ j by A3, A4, A25, A38, Def1 .= (((f | (j -' 1)) ^ <*p*>) ^ ((f /^ j) | (k -' 1))) /^ (len ((f | (j -' 1)) ^ <*p*>)) by A35, GENEALG1:2 .= (f /^ j) | ((i -' j) -' 1) by A27, FINSEQ_5:37 ; A42: (Replace (f,j,p)) | (j -' 1) = (((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j -' 1) by A3, A4, Def1 .= ((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (j -' 1) by FINSEQ_1:32 .= ((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (len (f | (j -' 1))) by A4, A33, FINSEQ_1:59, XXREAL_0:2 .= f | (j -' 1) by FINSEQ_5:23 ; A43: p = (Replace (f,j,p)) . j by A3, A4, Lm2 .= (Replace (f,j,p)) /. j by A34, PARTFUN1:def_6 ; A44: f . i = (Replace (f,j,p)) . i by A24, FUNCT_7:32 .= (Replace (f,j,p)) /. i by A40, PARTFUN1:def_6 ; A45: Swap ((Replace (f,j,p)),i,j) = Swap ((Replace (f,j,p)),j,i) by Th21 .= (((((Replace (f,j,p)) | (j -' 1)) ^ <*((Replace (f,j,p)) /. i)*>) ^ (((Replace (f,j,p)) /^ j) | ((i -' j) -' 1))) ^ <*((Replace (f,j,p)) /. j)*>) ^ ((Replace (f,j,p)) /^ i) by A3, A24, A39, Th27 .= ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*p*>) ^ (f /^ i) by A5, A36, A42, A41, A44, A43, PARTFUN1:def_6 ; A46: i -' j <> 0 by A26, XREAL_0:def_2; i -' 1 <= i by NAT_D:35; then i -' 1 <= len f by A2, XXREAL_0:2; then (i -' 1) -' j <= (len f) -' j by NAT_D:42; then (i -' 1) -' j <= len (f /^ j) by RFINSEQ:29; then i -' (1 + j) <= len (f /^ j) by NAT_2:30; then A47: (i -' j) -' 1 <= len (f /^ j) by NAT_2:30; then A48: len ((f /^ j) | ((i -' j) -' 1)) = k -' 1 by A27, FINSEQ_1:59; A49: len ((f | (j -' 1)) ^ <*(f /. i)*>) = (len (f | (j -' 1))) + (len <*(f /. i)*>) by FINSEQ_1:22 .= (len (f | (j -' 1))) + 1 by FINSEQ_1:39 .= (j -' 1) + 1 by A4, A32, FINSEQ_1:59, XXREAL_0:2 .= j by A3, XREAL_1:235 ; A50: i <= len (Swap (f,j,i)) by A2, Th18; A51: len (((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) = (len ((f /^ j) | ((i -' j) -' 1))) + (len <*(f /. j)*>) by FINSEQ_1:22 .= (len ((f /^ j) | ((i -' j) -' 1))) + 1 by FINSEQ_1:39 .= ((i -' j) -' 1) + 1 by A47, FINSEQ_1:59 .= i -' j by A46, NAT_1:14, XREAL_1:235 ; Replace ((Swap (f,i,j)),i,p) = Replace ((Swap (f,j,i)),i,p) by Th21 .= (((Swap (f,j,i)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))) /^ (j + k)) by A1, A25, A28, A50, Def1 .= (((Swap (f,j,i)) | (i -' 1)) ^ <*p*>) ^ (((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)) /^ (len (((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>))) by A27, A49, A51, FINSEQ_5:36 .= (((Swap (f,j,i)) | (k + (j -' 1))) ^ <*p*>) ^ (f /^ i) by A25, A30, FINSEQ_5:37 .= ((((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)))) | ((j -' 1) + k)) ^ <*p*>) ^ (f /^ i) by A28, FINSEQ_1:32 .= ((((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)))) | ((len (f | (j -' 1))) + k)) ^ <*p*>) ^ (f /^ i) by A4, A32, FINSEQ_1:59, XXREAL_0:2 .= (((f | (j -' 1)) ^ ((<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))) | k)) ^ <*p*>) ^ (f /^ i) by GENEALG1:2 .= (((f | (j -' 1)) ^ ((<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))) | ((len <*(f /. i)*>) + (k -' 1)))) ^ <*p*>) ^ (f /^ i) by A31, FINSEQ_1:39 .= (((f | (j -' 1)) ^ (<*(f /. i)*> ^ (((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)) | (k -' 1)))) ^ <*p*>) ^ (f /^ i) by GENEALG1:2 .= (((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ i))) | (k -' 1)))) ^ <*p*>) ^ (f /^ i) by FINSEQ_1:32 .= (((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((f /^ j) | ((i -' j) -' 1)))) ^ <*p*>) ^ (f /^ i) by A48, FINSEQ_5:23 .= ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*p*>) ^ (f /^ i) by FINSEQ_1:32 ; hence Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) by A45; ::_thesis: verum end; end; end; theorem Th33: :: FINSEQ_7:33 for D being non empty set for f being FinSequence of D for p being Element of D for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) let f be FinSequence of D; ::_thesis: for p being Element of D for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) let p be Element of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) let i, k, j be Nat; ::_thesis: ( i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) ) assume that A1: i <> k and A2: j <> k and A3: 1 <= i and A4: i <= len f and A5: 1 <= j and A6: j <= len f ; ::_thesis: Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) ( i <= len (Replace (f,k,p)) & j <= len (Replace (f,k,p)) ) by A4, A6, FUNCT_7:97; hence Swap ((Replace (f,k,p)),i,j) = Replace ((Replace ((Replace (f,k,p)),i,((Replace (f,k,p)) /. j))),j,((Replace (f,k,p)) /. i)) by A3, A5, Def2 .= Replace ((Replace ((Replace (f,k,p)),i,(f /. j))),j,((Replace (f,k,p)) /. i)) by A2, A5, A6, Th10 .= Replace ((Replace ((Replace (f,k,p)),i,(f /. j))),j,(f /. i)) by A1, A3, A4, Th10 .= Replace ((Replace ((Replace (f,i,(f /. j))),k,p)),j,(f /. i)) by A1, FUNCT_7:33 .= Replace ((Replace ((Replace (f,i,(f /. j))),j,(f /. i))),k,p) by A2, FUNCT_7:33 .= Replace ((Swap (f,i,j)),k,p) by A3, A4, A5, A6, Def2 ; ::_thesis: verum end; theorem :: FINSEQ_7:34 for D being non empty set for f being FinSequence of D for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j) let f be FinSequence of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j) let i, k, j be Nat; ::_thesis: ( i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f implies Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j) ) assume that A1: ( i <> k & j <> k ) and A2: 1 <= i and A3: i <= len f and A4: 1 <= j and A5: j <= len f and A6: 1 <= k and A7: k <= len f ; ::_thesis: Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j) A8: ( i <= len (Replace (f,i,(f /. k))) & j <= len (Replace (f,i,(f /. k))) ) by A3, A5, FUNCT_7:97; ( j <= len (Swap (f,i,j)) & k <= len (Swap (f,i,j)) ) by A5, A7, Th18; hence Swap ((Swap (f,i,j)),j,k) = Replace ((Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. k))),k,((Swap (f,i,j)) /. j)) by A4, A6, Def2 .= Replace ((Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. k))),k,(f /. i)) by A2, A3, A4, A5, Th31 .= Replace ((Replace ((Swap (f,i,j)),j,(f /. k))),k,(f /. i)) by A1, A6, A7, Th30 .= Replace ((Replace ((Swap (f,j,i)),j,(f /. k))),k,(f /. i)) by Th21 .= Replace ((Swap ((Replace (f,i,(f /. k))),j,i)),k,(f /. i)) by A2, A3, A4, A5, Th32 .= Swap ((Replace ((Replace (f,i,(f /. k))),k,(f /. i))),j,i) by A1, A2, A4, A8, Th33 .= Swap ((Swap (f,i,k)),j,i) by A2, A3, A6, A7, Def2 .= Swap ((Swap (f,i,k)),i,j) by Th21 ; ::_thesis: verum end; theorem :: FINSEQ_7:35 for D being non empty set for f being FinSequence of D for i, k, j, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, k, j, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) let f be FinSequence of D; ::_thesis: for i, k, j, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) let i, k, j, l be Nat; ::_thesis: ( i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f implies Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) ) assume that A1: ( i <> k & j <> k ) and A2: ( l <> i & l <> j ) and A3: 1 <= i and A4: i <= len f and A5: 1 <= j and A6: j <= len f and A7: 1 <= k and A8: k <= len f and A9: 1 <= l and A10: l <= len f ; ::_thesis: Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) A11: ( i <= len (Replace (f,k,(f /. l))) & j <= len (Replace (f,k,(f /. l))) ) by A4, A6, FUNCT_7:97; set F = Swap (f,i,j); ( k <= len (Swap (f,i,j)) & l <= len (Swap (f,i,j)) ) by A8, A10, Th18; then Swap ((Swap (f,i,j)),k,l) = Replace ((Replace ((Swap (f,i,j)),k,((Swap (f,i,j)) /. l))),l,((Swap (f,i,j)) /. k)) by A7, A9, Def2 .= Replace ((Replace ((Swap (f,i,j)),k,((Swap (f,i,j)) /. l))),l,(f /. k)) by A1, A7, A8, Th30 .= Replace ((Replace ((Swap (f,i,j)),k,(f /. l))),l,(f /. k)) by A2, A9, A10, Th30 .= Replace ((Replace ((Swap (f,j,i)),k,(f /. l))),l,(f /. k)) by Th21 .= Replace ((Swap ((Replace (f,k,(f /. l))),j,i)),l,(f /. k)) by A1, A3, A4, A5, A6, Th33 .= Swap ((Replace ((Replace (f,k,(f /. l))),l,(f /. k))),j,i) by A2, A3, A5, A11, Th33 .= Swap ((Swap (f,k,l)),j,i) by A7, A8, A9, A10, Def2 .= Swap ((Swap (f,k,l)),i,j) by Th21 ; hence Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) ; ::_thesis: verum end;