let D be 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)
let f be 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 i, j be Nat; ( 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
; 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)
; verum