let m, n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ;

let m, n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ;
:: original: seq
redefine func seq (m,n) -> ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) ;

for c, a, b being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) holds
( c : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) in seq (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ,b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) iff ( 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= c : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) & c : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) <= b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) + a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) set ) ) ) ;

for a being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) holds seq (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) = {} : ( ( ) ( ) set ) ;

for b, a being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) holds
( b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) or b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) + a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) set ) in seq (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ,b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) ) ;

for b1, b2, a being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) holds
( b1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) <= b2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) iff seq (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ,b1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) c= seq (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ,b2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) ) ;

for a, b being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) holds (seq (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ,b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) )) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) \/ {((a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) + b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty V12() 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element ) set ) : ( ( ) ( ) set ) = seq (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) ,(b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) number ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) ;

for m, n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds seq (m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non finite ) set ) ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) are_equipotent ;

let m, n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

let Al be ( ( ) ( Relation-like non empty ) QC-alphabet ) ;
let f be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

for m, n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds seq (m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) c= Seg (m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + b₂ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) ;

for n, m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds Seg n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) misses seq (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ;

for f, g being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) holds dom (f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ^ g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) set ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) = (dom f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) \/ (seq ((len f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len g : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds len (Sgm (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds dom (Sgm (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) = dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds rng (Sgm (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) = seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for i being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) in dom (Sgm (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) holds
(Sgm (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = (len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) c= dom (g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ^ f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds dom ((g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ^ f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) | (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like FinSubsequence-like ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) : ( ( ) ( non finite ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) = seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds Seq ((g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ^ f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) | (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like FinSubsequence-like ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) : ( ( ) ( non finite ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) set ) = (Sgm (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ^ f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) : ( ( ) ( non finite ) set ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for g, f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds dom (Seq ((g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ^ f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) | (seq ((len g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( finite ) Subset of ( ( ) ( non finite ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like FinSubsequence-like ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) : ( ( ) ( non finite ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) set ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) = dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) ;

for Al being ( ( ) ( Relation-like non empty ) QC-alphabet )
for f, g being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) is_Subsequence_of g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ^ f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) : ( ( ) ( non empty ) Element of K19((QC-WFF b₁ : ( ( ) ( Relation-like non empty ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

let D be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) ;
let P be ( ( Function-like quasi_total bijective ) ( Relation-like dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) -defined dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) -valued Function-like one-to-one V14( dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) ) quasi_total onto bijective ) Permutation of dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined D : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non finite ) set ) ) ) ;