:: RINFSUP1 semantic presentation

REAL is non empty V52() V53() V54() V58() V71() V90() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() V90() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V52() V58() V71() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{0,1} is non empty V52() V53() V54() V55() V56() V57() set
INT is non empty V52() V53() V54() V55() V56() V58() V71() set
RAT is non empty V52() V53() V54() V55() V58() V71() set
omega is non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() V90() set
K6(omega) is set
K6(NAT) is set
K7(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(COMPLEX,REAL)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
ExtREAL is non empty V53() set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() V69() V70() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 is V11() real ext-real set
seq2 is V11() real ext-real set
seq1 is V11() real ext-real set
seq2 + seq1 is V11() real ext-real set
seq1 - seq1 is V11() real ext-real set
seq1 + 0 is V11() real ext-real Element of REAL
seq1 is V11() real ext-real set
seq2 is V11() real ext-real set
seq1 - seq2 is V11() real ext-real set
seq1 + seq2 is V11() real ext-real set
seq1 is V11() real ext-real set
seq1 - seq1 is V11() real ext-real set
abs (seq1 - seq1) is V11() real ext-real Element of REAL
- seq2 is V11() real ext-real set
(- seq2) + seq1 is V11() real ext-real set
- seq2 is V11() real ext-real set
seq1 + (- seq2) is V11() real ext-real set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 + seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1 + seq2) - seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- seq2 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive set
(- 1) * seq2 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(seq1 + seq2) + (- seq2) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
((seq1 + seq2) - seq2) . seq1 is V11() real ext-real Element of REAL
seq1 . seq1 is V11() real ext-real Element of REAL
seq2 - seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 + (- seq2) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
seq1 + (seq2 - seq2) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1 + (seq2 - seq2)) . seq1 is V11() real ext-real Element of REAL
- seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 + (- seq2) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2 + (- seq2)) . seq1 is V11() real ext-real Element of REAL
(seq1 . seq1) + ((seq2 + (- seq2)) . seq1) is V11() real ext-real Element of REAL
seq2 . seq1 is V11() real ext-real Element of REAL
(- seq2) . seq1 is V11() real ext-real Element of REAL
(seq2 . seq1) + ((- seq2) . seq1) is V11() real ext-real Element of REAL
(seq1 . seq1) + ((seq2 . seq1) + ((- seq2) . seq1)) is V11() real ext-real Element of REAL
- (seq2 . seq1) is V11() real ext-real Element of REAL
(seq2 . seq1) + (- (seq2 . seq1)) is V11() real ext-real Element of REAL
(seq1 . seq1) + ((seq2 . seq1) + (- (seq2 . seq1))) is V11() real ext-real Element of REAL
seq1 is V11() real ext-real set
- seq1 is V11() real ext-real set
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng seq2 is V52() V53() V54() Element of K6(REAL)
- seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real non positive set
(- 1) * seq2 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
rng (- seq2) is V52() V53() V54() Element of K6(REAL)
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq1 is V11() real ext-real Element of REAL
(- seq2) . seq1 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(- seq2) . seq1 is V11() real ext-real Element of REAL
- ((- seq2) . seq1) is V11() real ext-real Element of REAL
seq2 . seq1 is V11() real ext-real Element of REAL
- (seq2 . seq1) is V11() real ext-real Element of REAL
- (- (seq2 . seq1)) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real non positive set
(- 1) * seq1 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
rng (- seq1) is V52() V53() V54() Element of K6(REAL)
rng seq1 is V52() V53() V54() Element of K6(REAL)
-- (rng seq1) is V52() V53() V54() set
-- (rng seq1) is V53() set
seq2 is set
seq1 is V11() real ext-real Element of REAL
- seq1 is V11() real ext-real Element of REAL
- (- seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(- 1) * (- seq1) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
rng (- (- seq1)) is V52() V53() V54() Element of K6(REAL)
- (- seq1) is V11() real ext-real Element of REAL
seq2 is set
seq1 is V11() real ext-real Element of REAL
- seq1 is V11() real ext-real Element of REAL
-- (-- (rng seq1)) is V52() V53() V54() set
-- (-- (rng seq1)) is V53() set
- (- seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng seq1 is V52() V53() V54() Element of K6(REAL)
seq2 is V11() real ext-real set
seq1 is ext-real set
dom seq1 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq2 is set
seq1 . seq2 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
seq1 is V11() real ext-real set
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq1 is V11() real ext-real Element of REAL
seq2 + 1 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng seq1 is V52() V53() V54() Element of K6(REAL)
seq2 is V11() real ext-real set
seq1 is ext-real set
dom seq1 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq2 is set
seq1 . seq2 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
seq1 is V11() real ext-real set
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq1 is V11() real ext-real Element of REAL
seq2 - 1 is V11() real ext-real Element of REAL
seq1 is V11() real ext-real set
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq2) is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
seq1 - seq2 is V11() real ext-real set
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq3 is V11() real ext-real Element of REAL
seq4 is V11() real ext-real set
seq5 is V11() real ext-real set
seq2 is V11() real ext-real set
dom seq2 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq3 is set
seq2 . seq3 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
seq1 - seq2 is V11() real ext-real set
seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq4 is V11() real ext-real Element of REAL
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq5 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq1 - seq3 is V11() real ext-real set
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq1 - seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq4 is V11() real ext-real Element of REAL
seq5 is V11() real ext-real set
seq1 - seq5 is V11() real ext-real set
seq1 is V11() real ext-real set
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq2) is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
seq1 + seq2 is V11() real ext-real set
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq3 is V11() real ext-real Element of REAL
seq4 is V11() real ext-real set
seq5 is V11() real ext-real set
seq2 is V11() real ext-real set
dom seq2 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq3 is set
seq2 . seq3 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
seq1 + seq2 is V11() real ext-real set
seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq4 is V11() real ext-real Element of REAL
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq5 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq1 + seq3 is V11() real ext-real set
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq1 + seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq4 is V11() real ext-real Element of REAL
seq5 is V11() real ext-real set
seq1 + seq5 is V11() real ext-real set
seq1 is V11() real ext-real set
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq2) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 + 1 is V11() real ext-real Element of REAL
(seq2) - seq1 is V11() real ext-real Element of REAL
(seq2) - ((seq2) - seq1) is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 is V11() real ext-real set
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq2) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 - 1 is V11() real ext-real Element of REAL
seq1 - (seq2) is V11() real ext-real Element of REAL
(seq2) + (seq1 - (seq2)) is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq2 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real non positive set
(- 1) * seq1 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
seq1 is V11() real ext-real set
- seq1 is V11() real ext-real set
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
(- seq1) . seq2 is V11() real ext-real Element of REAL
- (seq1 . seq2) is V11() real ext-real Element of REAL
- ((- seq1) . seq2) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real non positive set
(- 1) * seq1 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
- (- seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(- 1) * (- seq1) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq1) is V11() real ext-real Element of REAL
- seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real non positive set
(- 1) * seq1 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
((- seq1)) is V11() real ext-real Element of REAL
rng (- seq1) is V52() V53() V54() Element of K6(REAL)
lower_bound (rng (- seq1)) is V11() real ext-real Element of REAL
- ((- seq1)) is V11() real ext-real Element of REAL
-- (rng seq1) is V52() V53() V54() set
-- (rng seq1) is V53() set
lower_bound (-- (rng seq1)) is V11() real ext-real set
- (lower_bound (-- (rng seq1))) is V11() real ext-real set
- (lower_bound (rng (- seq1))) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq1) is V11() real ext-real Element of REAL
- seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real non positive set
(- 1) * seq1 is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
((- seq1)) is V11() real ext-real Element of REAL
rng (- seq1) is V52() V53() V54() Element of K6(REAL)
upper_bound (rng (- seq1)) is V11() real ext-real Element of REAL
- ((- seq1)) is V11() real ext-real Element of REAL
-- (rng seq1) is V52() V53() V54() set
-- (rng seq1) is V53() set
upper_bound (-- (rng seq1)) is V11() real ext-real set
- (upper_bound (-- (rng seq1))) is V11() real ext-real set
- (upper_bound (rng (- seq1))) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq1) is V11() real ext-real Element of REAL
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq2) is V11() real ext-real Element of REAL
(seq1) + (seq2) is V11() real ext-real Element of REAL
seq1 + seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((seq1 + seq2)) is V11() real ext-real Element of REAL
rng (seq1 + seq2) is V52() V53() V54() Element of K6(REAL)
lower_bound (rng (seq1 + seq2)) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq1 + seq2) . seq1 is V11() real ext-real Element of REAL
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 . seq1 is V11() real ext-real Element of REAL
(seq1 . seq1) + (seq2 . seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq1) is V11() real ext-real Element of REAL
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 + seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((seq1 + seq2)) is V11() real ext-real Element of REAL
rng (seq1 + seq2) is V52() V53() V54() Element of K6(REAL)
upper_bound (rng (seq1 + seq2)) is V11() real ext-real Element of REAL
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq2) is V11() real ext-real Element of REAL
(seq1) + (seq2) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq1 + seq2) . seq1 is V11() real ext-real Element of REAL
seq2 . seq1 is V11() real ext-real Element of REAL
seq1 . seq1 is V11() real ext-real Element of REAL
(seq1 . seq1) + (seq2 . seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
seq2 is V11() real ext-real set
K87(seq1) is V52() V53() V54() set
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq1 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq2
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq2 ^\ seq1) . seq1 is V11() real ext-real Element of REAL
seq1 + seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . (seq1 + seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq1) is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq1) is V11() real ext-real Element of REAL
seq1 . 0 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq1) is V11() real ext-real Element of REAL
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 (#) seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq2) is V11() real ext-real Element of REAL
(seq1) * (seq2) is V11() real ext-real Element of REAL
((seq1 (#) seq2)) is V11() real ext-real Element of REAL
rng (seq1 (#) seq2) is V52() V53() V54() Element of K6(REAL)
lower_bound (rng (seq1 (#) seq2)) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq1 (#) seq2) . seq1 is V11() real ext-real Element of REAL
seq1 . seq1 is V11() real ext-real Element of REAL
seq2 . seq1 is V11() real ext-real Element of REAL
(seq1 . seq1) * (seq2 . seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq1) is V11() real ext-real Element of REAL
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 (#) seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((seq1 (#) seq2)) is V11() real ext-real Element of REAL
rng (seq1 (#) seq2) is V52() V53() V54() Element of K6(REAL)
upper_bound (rng (seq1 (#) seq2)) is V11() real ext-real Element of REAL
(seq2) is V11() real ext-real Element of REAL
rng seq2 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq2) is V11() real ext-real Element of REAL
(seq1) * (seq2) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq1 (#) seq2) . seq1 is V11() real ext-real Element of REAL
seq1 . seq1 is V11() real ext-real Element of REAL
seq2 . seq1 is V11() real ext-real Element of REAL
(seq1 . seq1) * (seq2 . seq1) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim seq1 is V11() real ext-real Element of REAL
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq1) is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim seq1 is V11() real ext-real Element of REAL
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq1) is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq2
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq2
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq2
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq2 is set
seq3 is set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq4 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq2
rng (seq2 ^\ seq1) is V52() V53() V54() Element of K6(REAL)
{ (seq2 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 <= b₁ } is set
seq3 is set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . seq4 is V11() real ext-real Element of REAL
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq2 ^\ seq1) . n is V11() real ext-real Element of REAL
dom (seq2 ^\ seq1) is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq3 is set
seq4 is set
(seq2 ^\ seq1) . seq4 is V11() real ext-real Element of REAL
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 . (seq1 + seq5) is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq1 ^\ seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq1
rng (seq1 ^\ seq2) is V52() V53() V54() Element of K6(REAL)
seq2 is V52() V53() V54() Element of K6(REAL)
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq1 ^\ seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq1
rng (seq1 ^\ seq2) is V52() V53() V54() Element of K6(REAL)
seq2 is V52() V53() V54() Element of K6(REAL)
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq1 is V52() V53() V54() Element of K6(REAL)
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq1 . seq2 is V11() real ext-real Element of REAL
seq1 is V11() real ext-real set
seq2 is V11() real ext-real set
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq3 is V11() real ext-real Element of REAL
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq2 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound seq1 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
(seq1 . seq2) + seq2 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq1 . seq2 is V11() real ext-real Element of REAL
seq1 is V11() real ext-real set
seq2 is V11() real ext-real set
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq3 is V11() real ext-real Element of REAL
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq2 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound seq1 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real set
(seq1 . seq2) - seq2 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : a₁ <= b₁ } is set
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound seq1 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real Element of REAL
seq3 is V52() V53() V54() Element of K6(REAL)
lower_bound seq3 is V11() real ext-real Element of REAL
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is set
seq2 . seq2 is V11() real ext-real Element of REAL
seq1 . seq2 is V11() real ext-real Element of REAL
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq3 <= b₁ } is set
seq2 . seq3 is V11() real ext-real Element of REAL
seq4 is V52() V53() V54() Element of K6(REAL)
lower_bound seq4 is V11() real ext-real Element of REAL
dom seq2 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
dom seq1 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : a₁ <= b₁ } is set
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq2 <= b₁ } is set
seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound seq1 is V11() real ext-real Element of REAL
seq2 is V11() real ext-real Element of REAL
seq3 is V52() V53() V54() Element of K6(REAL)
upper_bound seq3 is V11() real ext-real Element of REAL
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is set
seq2 . seq2 is V11() real ext-real Element of REAL
seq1 . seq2 is V11() real ext-real Element of REAL
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq3 <= b₁ } is set
seq2 . seq3 is V11() real ext-real Element of REAL
seq4 is V52() V53() V54() Element of K6(REAL)
upper_bound seq4 is V11() real ext-real Element of REAL
dom seq2 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
dom seq1 is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) . seq1 is V11() real ext-real Element of REAL
seq2 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq2
((seq2 ^\ seq1)) is V11() real ext-real Element of REAL
rng (seq2 ^\ seq1) is V52() V53() V54() Element of K6(REAL)
lower_bound (rng (seq2 ^\ seq1)) is V11() real ext-real Element of REAL
{ (seq2 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 <= b₁ } is set
seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound seq1 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) . seq1 is V11() real ext-real Element of REAL
seq2 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq2
((seq2 ^\ seq1)) is V11() real ext-real Element of REAL
rng (seq2 ^\ seq1) is V52() V53() V54() Element of K6(REAL)
upper_bound (rng (seq2 ^\ seq1)) is V11() real ext-real Element of REAL
{ (seq2 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 <= b₁ } is set
seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound seq1 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . 0 is V11() real ext-real Element of REAL
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
lower_bound (rng seq1) is V11() real ext-real Element of REAL
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : 0 <= b₁ } is set
seq2 is V52() V53() V54() Element of K6(REAL)
lower_bound seq2 is V11() real ext-real Element of REAL
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . 0 is V11() real ext-real Element of REAL
(seq1) is V11() real ext-real Element of REAL
rng seq1 is V52() V53() V54() Element of K6(REAL)
upper_bound (rng seq1) is V11() real ext-real Element of REAL
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : 0 <= b₁ } is set
seq2 is V52() V53() V54() Element of K6(REAL)
upper_bound seq2 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is V11() real ext-real set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . seq1 is V11() real ext-real Element of REAL
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 <= b₁ } is set
seq2 is V52() V53() V54() Element of K6(REAL)
lower_bound seq2 is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq2 + seq3 is V11() real ext-real set
seq4 is V11() real ext-real set
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq5 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq3) is V11() real ext-real Element of REAL
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq3) is V11() real ext-real Element of REAL
seq4 is V11() real ext-real set
seq2 + seq4 is V11() real ext-real set
seq3 is V11() real ext-real set
seq2 + seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq4) is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq4 is V11() real ext-real Element of REAL
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
lower_bound seq2 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is V11() real ext-real set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . seq1 is V11() real ext-real Element of REAL
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 <= b₁ } is set
seq2 is V52() V53() V54() Element of K6(REAL)
upper_bound seq2 is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq2 - seq3 is V11() real ext-real set
seq4 is V11() real ext-real set
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq5 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq3) is V11() real ext-real Element of REAL
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq3) is V11() real ext-real Element of REAL
seq4 is V11() real ext-real set
seq2 - seq4 is V11() real ext-real set
seq3 is V11() real ext-real set
seq2 - seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq4) is V11() real ext-real Element of REAL
seq3 is V11() real ext-real set
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq4 is V11() real ext-real Element of REAL
seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + seq5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
upper_bound seq2 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is V11() real ext-real set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . seq1 is V11() real ext-real Element of REAL
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 <= b₁ } is set
seq1 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq1
rng (seq1 ^\ seq1) is V52() V53() V54() Element of K6(REAL)
seq2 is V52() V53() V54() Element of K6(REAL)
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq1 ^\ seq1) . seq4 is V11() real ext-real Element of REAL
seq5 is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . n is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
((seq1 ^\ seq1)) is V11() real ext-real Element of REAL
lower_bound (rng (seq1 ^\ seq1)) is V11() real ext-real Element of REAL
lower_bound seq2 is V11() real ext-real Element of REAL
lower_bound seq2 is V11() real ext-real Element of REAL
((seq1 ^\ seq1)) is V11() real ext-real Element of REAL
lower_bound (rng (seq1 ^\ seq1)) is V11() real ext-real Element of REAL
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq4) is V11() real ext-real Element of REAL
dom (seq1 ^\ seq1) is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq5 is set
(seq1 ^\ seq1) . seq5 is V11() real ext-real Element of REAL
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq4) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is V11() real ext-real set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . seq1 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq2) is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is V11() real ext-real set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . seq1 is V11() real ext-real Element of REAL
{ (seq1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 <= b₁ } is set
seq1 ^\ seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of seq1
rng (seq1 ^\ seq1) is V52() V53() V54() Element of K6(REAL)
seq2 is V52() V53() V54() Element of K6(REAL)
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
(seq1 ^\ seq1) . seq4 is V11() real ext-real Element of REAL
seq5 is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . n is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
((seq1 ^\ seq1)) is V11() real ext-real Element of REAL
upper_bound (rng (seq1 ^\ seq1)) is V11() real ext-real Element of REAL
upper_bound seq2 is V11() real ext-real Element of REAL
upper_bound seq2 is V11() real ext-real Element of REAL
((seq1 ^\ seq1)) is V11() real ext-real Element of REAL
upper_bound (rng (seq1 ^\ seq1)) is V11() real ext-real Element of REAL
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq4) is V11() real ext-real Element of REAL
dom (seq1 ^\ seq1) is V52() V53() V54() V55() V56() V57() Element of K6(NAT)
seq5 is set
(seq1 ^\ seq1) . seq5 is V11() real ext-real Element of REAL
seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq4) is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is V11() real ext-real set
seq1 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq1) . seq1 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . (seq1 + seq2) is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
seq1 + seq3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 . seq2 is V11() real ext-real Element of REAL
seq1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT
seq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(seq2) . seq1 is V11() real ext-real Element of REAL
(seq2) . (seq1 + 1) is V11() real ext-real Element of REAL
seq2 . seq1 is V11() real ext-real Element of REAL
min (((seq2) . (seq1 + 1)),(seq2 . seq1)) is V11() real ext-real set
{ (seq2 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54() V55() V56() V57() V69() V70() Element of NAT : seq1 + 1 <= b₁ } is set
{ (seq2 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V52() V53() V54()