:: FINSEQ_7 semantic presentation

begin

theorem :: FINSEQ_7:1
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) < j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds
f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = ((((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | (i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ) set ) *> : ( ( Relation-like Function-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V34() FinSequence-like FinSubsequence-like ) set ) ^ ((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | ((j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V34() FinSequence-like FinSubsequence-like ) set ) ^ <*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) . j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ) set ) *> : ( ( Relation-like Function-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V34() FinSequence-like FinSubsequence-like ) set ) ^ (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V34() FinSequence-like FinSubsequence-like ) set ) ;

theorem :: FINSEQ_7:2
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat)
for f, g, h being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) st len g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len h : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & len g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) < i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len (g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ^ f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) set ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
(g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ^ f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) set ) . i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) set ) = (h : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ^ f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) set ) . i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) set ) ;

theorem :: FINSEQ_7:3
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat)
for f, g being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) . i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) set ) = (g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ^ f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) set ) . ((len g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: FINSEQ_7:4
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, n being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) in dom (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ n : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ n : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) set ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) . (n : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) + i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ext-real V31() V32() V33() ) set ) : ( ( ) ( ) set ) ;

begin

notation
let D be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) ;
let i be ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ;
let p be ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ;
synonym Replace (f,i,p) for D +* (f,i);
end;

definition
let D be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) ;
let i be ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ;
let p be ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ;
:: original: Replace
redefine func Replace (f,i,p) -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ext-real ) ( ext-real ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ext-real ) ( ext-real ) set ) ) equals :: FINSEQ_7:def 1
((f : ( ( ext-real ) ( ext-real ) set ) | (i : ( ( ) ( ) set ) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ext-real ) ( ext-real ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ext-real ) ( ext-real ) set ) ) ^ <*p : ( ( ) ( ) set ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ext-real ) ( ext-real ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ext-real ) ( ext-real ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ext-real ) ( ext-real ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ext-real ) ( ext-real ) set ) ) ^ (f : ( ( ext-real ) ( ext-real ) set ) /^ i : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ext-real ) ( ext-real ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ext-real ) ( ext-real ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ext-real ) ( ext-real ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ext-real ) ( ext-real ) set ) ) if ( 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( ) set ) & i : ( ( ) ( ) set ) <= len f : ( ( ext-real ) ( ext-real ) set ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )
otherwise f : ( ( ext-real ) ( ext-real ) set ) ;
end;

theorem :: FINSEQ_7:5
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds len (Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: FINSEQ_7:6
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds rng (Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) c= (rng f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) \/ {p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: FINSEQ_7:7
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in rng (Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

theorem :: FINSEQ_7:8
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:9
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
for k being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) < k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= (len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) - i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ext-real V31() V32() V33() ) set ) holds
(Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) . (i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) + k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ext-real V31() V32() V33() ) set ) : ( ( ) ( ) set ) = (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) . k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) set ) ;

theorem :: FINSEQ_7:10
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for k, i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds
(Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:11
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for q, p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) < j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Replace ((Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = ((((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | (i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ ((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | ((j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:12
for D being ( ( non empty ) ( non empty ) set )
for p, q being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Replace (<*p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:13
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, q being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Replace (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:14
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, q being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Replace (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:15
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, p3, q being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Replace (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:16
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, p3, q being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Replace (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:17
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, p3, q being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Replace (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

begin

registration
let f be ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence) ;
let i, j be ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ;
cluster Swap (f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) set ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) set ) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) -> FinSequence-like ;
end;

definition
let D be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) ;
let i, j be ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ;
:: original: Swap
redefine func Swap (f,i,j) -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ) ( ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ) ( ) set ) ) equals :: FINSEQ_7:def 2
 Replace ((Replace (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) set ) ,(f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) /. j : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of D : ( ( ) ( ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ) ( ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ) ( ) set ) ) ,j : ( ( ) ( ) set ) ,(f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) /. i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) set ) ) : ( ( ) ( ) Element of D : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( ) ( ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ) ( ) set ) ) if ( 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) set ) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) set ) <= len f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j : ( ( ) ( ) set ) & j : ( ( ) ( ) set ) <= len f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )
otherwise f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ;
end;

theorem :: FINSEQ_7:18
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds len (Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: FINSEQ_7:19
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:20
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds Swap ((Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:21
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:22
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) holds rng (Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) = rng f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

theorem :: FINSEQ_7:23
for D being ( ( non empty ) ( non empty ) set )
for p1, p2 being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Swap (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:24
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, p3 being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Swap (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:25
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, p3 being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Swap (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:26
for D being ( ( non empty ) ( non empty ) set )
for p1, p2, p3 being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds Swap (<*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = <*p1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(3 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:27
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) < j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = ((((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | (i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ ((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | ((j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:28
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) < i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = ((<*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ ((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | (i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' 2 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:29
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) < len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = (((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | (i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. (len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ ((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /^ i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) | (((len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -' i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -' 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ <*(f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() V41(1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:30
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, k, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:31
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( (Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) & (Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

begin

theorem :: FINSEQ_7:32
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Replace ((Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = Swap ((Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:33
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for i, k, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Swap ((Replace (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = Replace ((Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,p : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:34
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, k, j being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Swap ((Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = Swap ((Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: FINSEQ_7:35
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i, k, j, l being ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) st i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & l : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & l : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <> j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= l : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) & l : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
Swap ((Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,l : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) = Swap ((Swap (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,k : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,l : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ,j : ( ( V30() ) ( ext-real V24() V25() V26() V30() V31() V32() V33() ) Nat) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;