:: PRGCOR_2 semantic presentation

REAL is non empty V42() V65() V66() V67() V71() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V42() V47() V48() V65() V66() V67() V68() V69() V70() V71() Element of K11(REAL)
K11(REAL) is V42() set
COMPLEX is non empty V42() V65() V71() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V42() V47() V48() V65() V66() V67() V68() V69() V70() V71() set
K11(NAT) is V42() set
K11(NAT) is V42() set
RAT is non empty V42() V65() V66() V67() V68() V71() set
INT is non empty V42() V65() V66() V67() V68() V69() V71() set
K12(COMPLEX,COMPLEX) is V42() complex-yielding set
K11(K12(COMPLEX,COMPLEX)) is V42() set
K12(K12(COMPLEX,COMPLEX),COMPLEX) is V42() complex-yielding set
K11(K12(K12(COMPLEX,COMPLEX),COMPLEX)) is V42() set
K12(REAL,REAL) is V42() complex-yielding V55() V56() set
K11(K12(REAL,REAL)) is V42() set
K12(K12(REAL,REAL),REAL) is V42() complex-yielding V55() V56() set
K11(K12(K12(REAL,REAL),REAL)) is V42() set
K12(RAT,RAT) is RAT -valued V42() complex-yielding V55() V56() set
K11(K12(RAT,RAT)) is V42() set
K12(K12(RAT,RAT),RAT) is RAT -valued V42() complex-yielding V55() V56() set
K11(K12(K12(RAT,RAT),RAT)) is V42() set
K12(INT,INT) is RAT -valued INT -valued V42() complex-yielding V55() V56() set
K11(K12(INT,INT)) is V42() set
K12(K12(INT,INT),INT) is RAT -valued INT -valued V42() complex-yielding V55() V56() set
K11(K12(K12(INT,INT),INT)) is V42() set
K12(NAT,NAT) is RAT -valued INT -valued V42() complex-yielding V55() V56() V57() set
K12(K12(NAT,NAT),NAT) is RAT -valued INT -valued V42() complex-yielding V55() V56() V57() set
K11(K12(K12(NAT,NAT),NAT)) is V42() set
{} is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() functional integer V42() V47() V49( {} ) FinSequence-membered V65() V66() V67() V68() V69() V70() V71() set
1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
3 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() functional integer V42() V47() V49( {} ) FinSequence-membered V64() V65() V66() V67() V68() V69() V70() V71() Element of NAT
<*> REAL is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() Relation-like NAT -defined REAL -valued Function-like functional integer V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V53() complex-yielding V55() V56() V57() V65() V66() V67() V68() V69() V70() V71() FinSequence of REAL
- (<*> REAL) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (<*> REAL) is ext-real V14() V15() Element of REAL
a is non empty set
a is non empty set
b is T-Sequence-like Relation-like NAT -defined a -valued Function-like V42() V53() set
b . 0 is set
len b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
XFS2FS* b is Relation-like NAT -defined a -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of a
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len (XFS2FS* b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
(XFS2FS* b) . k is set
b . k is set
a is set
b is set
m is set
k is set
Fb is set
Fa is set
a is non empty set
b is Relation-like NAT -defined a -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of a
len b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fb is set
Fa is Element of a
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
c2 is T-Sequence-like Relation-like NAT -defined Function-like V42() V53() set
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 is T-Sequence-like Relation-like NAT -defined Function-like V42() V53() set
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
rng c2 is set
p is set
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V65() V66() V67() V68() V69() V70() Element of K11(NAT)
p2 is set
c2 . p2 is set
c is epsilon-transitive epsilon-connected ordinal set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
c2 . n is set
b . n is set
(n,(len b),(b . n),(b . n),Fa) is set
IFEQ (n,0,Fa,(n,(len b),(b . n),(b . n),Fa)) is set
b . p2 is set
(p2,(len b),(b . p2),(b . p2),Fa) is set
IFEQ (p2,0,Fa,(p2,(len b),(b . p2),(b . p2),Fa)) is set
b . p2 is set
(p2,(len b),(b . p2),(b . p2),Fa) is set
IFEQ (p2,0,Fa,(p2,(len b),(b . p2),(b . p2),Fa)) is set
0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len b) is V42() V49( len b) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom b is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
rng b is set
0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len b) is V42() V49( len b) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom b is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
rng b is set
p is T-Sequence-like Relation-like NAT -defined a -valued Function-like V42() V53() set
Replace (p,0,Fa) is T-Sequence-like Relation-like NAT -defined a -valued Function-like V42() V53() set
p2 is T-Sequence-like Relation-like NAT -defined a -valued Function-like V42() V53() set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . c is set
b . c is set
p . c is set
(c,(len b),(b . c),(b . c),Fa) is set
IFEQ (c,0,Fa,(c,(len b),(b . c),(b . c),Fa)) is set
len p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . 0 is set
b is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
b . 0 is ext-real V14() V15() Element of REAL
a is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
<%0%> is non empty V5() T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V42() V49(1) V53() complex-yielding V55() V56() V57() V58() V59() V60() V61() set
Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
m is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
m . (c2 + 1) is ext-real V14() V15() Element of REAL
m . c2 is ext-real V14() V15() Element of REAL
a . (c2 + 1) is ext-real V14() V15() Element of REAL
b . (c2 + 1) is ext-real V14() V15() Element of REAL
(a . (c2 + 1)) * (b . (c2 + 1)) is ext-real V14() V15() Element of REAL
(m . c2) + ((a . (c2 + 1)) * (b . (c2 + 1))) is ext-real V14() V15() Element of REAL
c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(c2 + 1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
p2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . 0 is ext-real V14() V15() Element of REAL
p2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . 0 is ext-real V14() V15() Element of REAL
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . p is ext-real V14() V15() Element of REAL
p + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
a . (p + 1) is ext-real V14() V15() Element of REAL
b . (p + 1) is ext-real V14() V15() Element of REAL
(a . (p + 1)) * (b . (p + 1)) is ext-real V14() V15() Element of REAL
(p2 . p) + ((a . (p + 1)) * (b . (p + 1))) is ext-real V14() V15() Element of REAL
c is ext-real V14() V15() Element of REAL
<%c%> is non empty V5() T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V49(1) V53() complex-yielding V55() V56() V58() V59() V60() V61() set
p2 ^ <%c%> is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
(p2 ^ <%c%>) . 0 is ext-real V14() V15() Element of REAL
p3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p3 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(p2 ^ <%c%>) . (p3 + 1) is ext-real V14() V15() Element of REAL
(p2 ^ <%c%>) . p3 is ext-real V14() V15() Element of REAL
a . (p3 + 1) is ext-real V14() V15() Element of REAL
b . (p3 + 1) is ext-real V14() V15() Element of REAL
(a . (p3 + 1)) * (b . (p3 + 1)) is ext-real V14() V15() Element of REAL
((p2 ^ <%c%>) . p3) + ((a . (p3 + 1)) * (b . (p3 + 1))) is ext-real V14() V15() Element of REAL
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V65() V66() V67() V68() V69() V70() Element of K11(NAT)
p2 . p3 is ext-real V14() V15() Element of REAL
p2 . (p3 + 1) is ext-real V14() V15() Element of REAL
<%((p2 . p) + ((a . (p + 1)) * (b . (p + 1))))%> is non empty V5() T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V49(1) V53() complex-yielding V55() V56() V58() V59() V60() V61() set
<%((p2 . p) + ((a . (p + 1)) * (b . (p + 1))))%> . 0 is ext-real V14() V15() Element of REAL
dom <%((p2 . p) + ((a . (p + 1)) * (b . (p + 1))))%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V49(1) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
(p3 + 1) + 0 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(p2 ^ <%c%>) . ((p3 + 1) + 0) is ext-real V14() V15() Element of REAL
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V65() V66() V67() V68() V69() V70() Element of K11(NAT)
len (p2 ^ <%c%>) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom (p2 ^ <%c%>) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
<%((p2 . p) + ((a . (p + 1)) * (b . (p + 1))))%> is non empty V5() T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V49(1) V53() complex-yielding V55() V56() V58() V59() V60() V61() set
len <%((p2 . p) + ((a . (p + 1)) * (b . (p + 1))))%> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom <%((p2 . p) + ((a . (p + 1)) * (b . (p + 1))))%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V49(1) set
(len p2) + (len <%((p2 . p) + ((a . (p + 1)) * (b . (p + 1))))%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(c2 + 1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
len m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
m . 0 is ext-real V14() V15() Element of REAL
0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(len a) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
((len a) -' 1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
c2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 . 0 is ext-real V14() V15() Element of REAL
c2 . Fb is ext-real V14() V15() Element of REAL
0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(len a) - 1 is ext-real V14() V15() integer Element of REAL
Fa is ext-real V14() V15() integer set
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
c2 . (p2 + 1) is ext-real V14() V15() Element of REAL
c2 . p2 is ext-real V14() V15() Element of REAL
a . (p2 + 1) is ext-real V14() V15() Element of REAL
b . (p2 + 1) is ext-real V14() V15() Element of REAL
(a . (p2 + 1)) * (b . (p2 + 1)) is ext-real V14() V15() Element of REAL
(c2 . p2) + ((a . (p2 + 1)) * (b . (p2 + 1))) is ext-real V14() V15() Element of REAL
Fa + 1 is ext-real V14() V15() integer Element of REAL
(Fa + 1) - 1 is ext-real V14() V15() integer Element of REAL
p is ext-real V14() V15() Element of REAL
p2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . 0 is ext-real V14() V15() Element of REAL
c is ext-real V14() V15() integer set
p2 . c is ext-real V14() V15() Element of REAL
m is ext-real V14() V15() Element of REAL
k is ext-real V14() V15() Element of REAL
Fb is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fb . 0 is ext-real V14() V15() Element of REAL
Fa is ext-real V14() V15() integer set
Fb . Fa is ext-real V14() V15() Element of REAL
Fb is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fb . 0 is ext-real V14() V15() Element of REAL
Fa is ext-real V14() V15() integer set
Fb . Fa is ext-real V14() V15() Element of REAL
c2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 . 0 is ext-real V14() V15() Element of REAL
p is ext-real V14() V15() integer set
c2 . p is ext-real V14() V15() Element of REAL
c2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 . 0 is ext-real V14() V15() Element of REAL
p is ext-real V14() V15() integer set
c2 . p is ext-real V14() V15() Element of REAL
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fb . c is ext-real V14() V15() Element of REAL
c2 . c is ext-real V14() V15() Element of REAL
c + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Fb . (c + 1) is ext-real V14() V15() Element of REAL
c2 . (c + 1) is ext-real V14() V15() Element of REAL
a . (c + 1) is ext-real V14() V15() Element of REAL
b . (c + 1) is ext-real V14() V15() Element of REAL
(a . (c + 1)) * (b . (c + 1)) is ext-real V14() V15() Element of REAL
(Fb . c) + ((a . (c + 1)) * (b . (c + 1))) is ext-real V14() V15() Element of REAL
a is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Sum a is ext-real V14() V15() Element of REAL
b is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
b . 0 is ext-real V14() V15() Element of REAL
b . (len a) is ext-real V14() V15() Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
a | m is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (a | m) is ext-real V14() V15() Element of REAL
b . m is ext-real V14() V15() Element of REAL
m + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
a | (m + 1) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (a | (m + 1)) is ext-real V14() V15() Element of REAL
b . (m + 1) is ext-real V14() V15() Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
k + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
a | Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (a | Fb) is ext-real V14() V15() Element of REAL
a /. Fb is ext-real V14() V15() Element of REAL
<*(a /. Fb)*> is non empty V5() Relation-like NAT -defined REAL -valued Function-like one-to-one V42() V49(1) FinSequence-like FinSubsequence-like complex-yielding V55() V56() V58() V59() V60() V61() FinSequence of REAL
(a | m) ^ <*(a /. Fb)*> is non empty Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Seg (len a) is V42() V49( len a) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom a is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
Seg Fb is V42() V49(Fb) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
len (a | Fb) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len (a | Fb)) is V42() V49( len (a | Fb)) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom (a | Fb) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
Fa is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum Fa is ext-real V14() V15() Element of REAL
c2 is ext-real V14() V15() Element of REAL
(b . m) + c2 is ext-real V14() V15() Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
<*c2*> is non empty V5() Relation-like NAT -defined REAL -valued Function-like one-to-one V42() V49(1) FinSequence-like FinSubsequence-like complex-yielding V55() V56() V58() V59() V60() V61() FinSequence of REAL
len <*c2*> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(len p) + (len <*c2*>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(len p) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(a | Fb) . Fb is ext-real V14() V15() Element of REAL
(a | Fb) /. Fb is ext-real V14() V15() Element of REAL
a . Fb is ext-real V14() V15() Element of REAL
a | 0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() Relation-like NAT -defined REAL -valued RAT -valued Function-like functional integer V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V53() complex-yielding V55() V56() V57() V65() V66() V67() V68() V69() V70() V71() FinSequence of REAL
Sum (a | 0) is ext-real V14() V15() Element of REAL
a | (len a) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (a | (len a)) is ext-real V14() V15() Element of REAL
a is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
(len a) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Sum a is ext-real V14() V15() Element of REAL
b is T-Sequence-like Relation-like NAT -defined Function-like V42() V53() set
len b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
b is T-Sequence-like Relation-like NAT -defined Function-like V42() V53() set
len b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
rng b is set
m is set
dom b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V65() V66() V67() V68() V69() V70() Element of K11(NAT)
k is set
b . k is set
Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
b . Fb is set
a | Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (a | Fb) is ext-real V14() V15() Element of REAL
m is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
k + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
m . (k + 1) is ext-real V14() V15() Element of REAL
m . k is ext-real V14() V15() Element of REAL
a . (k + 1) is ext-real V14() V15() Element of REAL
(m . k) + (a . (k + 1)) is ext-real V14() V15() Element of REAL
Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Fb + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
1 + Fb is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len a) is V42() V49( len a) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom a is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
m . Fb is ext-real V14() V15() Element of REAL
a | Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (a | Fb) is ext-real V14() V15() Element of REAL
Fa is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
a | Fa is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
a /. Fa is ext-real V14() V15() Element of REAL
<*(a /. Fa)*> is non empty V5() Relation-like NAT -defined REAL -valued Function-like one-to-one V42() V49(1) FinSequence-like FinSubsequence-like complex-yielding V55() V56() V58() V59() V60() V61() FinSequence of REAL
(a | Fb) ^ <*(a /. Fa)*> is non empty Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Sum (a | Fa) is ext-real V14() V15() Element of REAL
Sum <*(a /. Fa)*> is ext-real V14() V15() Element of REAL
(Sum (a | Fb)) + (Sum <*(a /. Fa)*>) is ext-real V14() V15() Element of REAL
(m . Fb) + (a /. Fa) is ext-real V14() V15() Element of REAL
a . Fa is ext-real V14() V15() Element of REAL
(m . Fb) + (a . Fa) is ext-real V14() V15() Element of REAL
m . 0 is ext-real V14() V15() Element of REAL
a | 0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() Relation-like NAT -defined REAL -valued RAT -valued Function-like functional integer V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V53() complex-yielding V55() V56() V57() V65() V66() V67() V68() V69() V70() V71() FinSequence of REAL
Sum (a | 0) is ext-real V14() V15() Element of REAL
m . (len a) is ext-real V14() V15() Element of REAL
a is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
b is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
|(a,b)| is ext-real V14() V15() Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
FS2XFS* (a,m) is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
FS2XFS* (b,m) is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
((FS2XFS* (a,m)),(FS2XFS* (b,m))) is ext-real V14() V15() Element of REAL
(len a) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
(FS2XFS* (b,m)) . 0 is ext-real V14() V15() Element of REAL
len (FS2XFS* (a,m)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom (FS2XFS* (a,m)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . 0 is ext-real V14() V15() Element of REAL
c is ext-real V14() V15() integer set
p2 . c is ext-real V14() V15() Element of REAL
Fb is Relation-like NAT -defined REAL -valued Function-like V42() V49( len a) FinSequence-like FinSubsequence-like complex-yielding V55() V56() Element of (len a) -tuples_on REAL
k is Relation-like NAT -defined REAL -valued Function-like V42() V49( len a) FinSequence-like FinSubsequence-like complex-yielding V55() V56() Element of (len a) -tuples_on REAL
mlt (Fb,k) is Relation-like NAT -defined REAL -valued Function-like V42() V49( len a) FinSequence-like FinSubsequence-like complex-yielding V55() V56() Element of (len a) -tuples_on REAL
len (mlt (Fb,k)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
mlt (a,b) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len (mlt (a,b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
n + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
p2 . (n + 1) is ext-real V14() V15() Element of REAL
p2 . n is ext-real V14() V15() Element of REAL
(mlt (a,b)) . (n + 1) is ext-real V14() V15() Element of REAL
(p2 . n) + ((mlt (a,b)) . (n + 1)) is ext-real V14() V15() Element of REAL
(FS2XFS* (a,m)) . (n + 1) is ext-real V14() V15() Element of REAL
a . (n + 1) is ext-real V14() V15() Element of REAL
(FS2XFS* (b,m)) . (n + 1) is ext-real V14() V15() Element of REAL
b . (n + 1) is ext-real V14() V15() Element of REAL
((FS2XFS* (a,m)) . (n + 1)) * ((FS2XFS* (b,m)) . (n + 1)) is ext-real V14() V15() Element of REAL
(p2 . n) + (((FS2XFS* (a,m)) . (n + 1)) * ((FS2XFS* (b,m)) . (n + 1))) is ext-real V14() V15() Element of REAL
Sum (mlt (a,b)) is ext-real V14() V15() Element of REAL
a is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
a . 0 is ext-real V14() V15() Element of REAL
len a is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
XFS2FS* a is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
b is ext-real V14() V15() Element of REAL
b * (XFS2FS* a) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
dom (b * (XFS2FS* a)) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom (XFS2FS* a) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
len (b * (XFS2FS* a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len (b * (XFS2FS* a))) is V42() V49( len (b * (XFS2FS* a))) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
len (XFS2FS* a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fa is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len Fa is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom Fa is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Replace (Fa,0,(a . 0)) is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
c2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 . p is ext-real V14() V15() Element of REAL
a . p is ext-real V14() V15() Element of REAL
b * (a . p) is ext-real V14() V15() Element of REAL
(XFS2FS* a) . p is ext-real V14() V15() Element of REAL
(b * (XFS2FS* a)) . p is ext-real V14() V15() Element of REAL
Fa . p is ext-real V14() V15() Element of REAL
Fb . p is ext-real V14() V15() Element of REAL
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
c2 . 0 is ext-real V14() V15() Element of REAL
p is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
XFS2FS* p is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
p . 0 is ext-real V14() V15() Element of REAL
p2 is ext-real V14() V15() integer set
len p is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len (XFS2FS* p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
c is ext-real V14() V15() integer set
c is ext-real V14() V15() integer set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
(XFS2FS* p) . n is ext-real V14() V15() Element of REAL
Fb . n is ext-real V14() V15() Element of REAL
p3 is ext-real V14() V15() integer set
a . n is ext-real V14() V15() Element of REAL
(XFS2FS* a) . n is ext-real V14() V15() Element of REAL
p . n is ext-real V14() V15() Element of REAL
b * (a . n) is ext-real V14() V15() Element of REAL
a is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
a . 0 is ext-real V14() V15() Element of REAL
len a is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
XFS2FS* a is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
- (XFS2FS* a) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
dom (- (XFS2FS* a)) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom (XFS2FS* a) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
len (- (XFS2FS* a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len (- (XFS2FS* a))) is V42() V49( len (- (XFS2FS* a))) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
len (XFS2FS* a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
k is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fb is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom Fb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Replace (Fb,0,(a . 0)) is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
Fa is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fa . c2 is ext-real V14() V15() Element of REAL
a . c2 is ext-real V14() V15() Element of REAL
- (a . c2) is ext-real V14() V15() Element of REAL
(XFS2FS* a) . c2 is ext-real V14() V15() Element of REAL
(- (XFS2FS* a)) . c2 is ext-real V14() V15() Element of REAL
Fb . c2 is ext-real V14() V15() Element of REAL
k . c2 is ext-real V14() V15() Element of REAL
len Fa is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom Fa is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fa . 0 is ext-real V14() V15() Element of REAL
c2 is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
XFS2FS* c2 is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
c2 . 0 is ext-real V14() V15() Element of REAL
p is ext-real V14() V15() integer set
len c2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len (XFS2FS* c2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
p2 is ext-real V14() V15() integer set
p2 is ext-real V14() V15() integer set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
(XFS2FS* c2) . c is ext-real V14() V15() Element of REAL
k . c is ext-real V14() V15() Element of REAL
n is ext-real V14() V15() integer set
a . c is ext-real V14() V15() Element of REAL
(XFS2FS* a) . c is ext-real V14() V15() Element of REAL
c2 . c is ext-real V14() V15() Element of REAL
- (a . c) is ext-real V14() V15() Element of REAL
b is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
b . 0 is ext-real V14() V15() Element of REAL
a is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len a is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len b is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
a . 0 is ext-real V14() V15() Element of REAL
XFS2FS* a is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
XFS2FS* b is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
(XFS2FS* a) + (XFS2FS* b) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fa is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Fa + Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len (XFS2FS* a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
len (XFS2FS* b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
c2 is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
Seg (len (XFS2FS* b)) is V42() V49( len (XFS2FS* b)) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom ((XFS2FS* a) + (XFS2FS* b)) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom (XFS2FS* b) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
Seg (len c2) is V42() V49( len c2) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Replace (p,0,(b . 0)) is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
p2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . c is ext-real V14() V15() Element of REAL
a . c is ext-real V14() V15() Element of REAL
b . c is ext-real V14() V15() Element of REAL
(a . c) + (b . c) is ext-real V14() V15() Element of REAL
(XFS2FS* a) . c is ext-real V14() V15() Element of REAL
(XFS2FS* b) . c is ext-real V14() V15() Element of REAL
((XFS2FS* a) + (XFS2FS* b)) . c is ext-real V14() V15() Element of REAL
p . c is ext-real V14() V15() Element of REAL
c2 . c is ext-real V14() V15() Element of REAL
len p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . 0 is ext-real V14() V15() Element of REAL
c is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
XFS2FS* c is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
c . 0 is ext-real V14() V15() Element of REAL
n is ext-real V14() V15() integer set
len c is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len (XFS2FS* c) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
p3 is ext-real V14() V15() integer set
p3 is ext-real V14() V15() integer set
k3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
(XFS2FS* c) . k3 is ext-real V14() V15() Element of REAL
c2 . k3 is ext-real V14() V15() Element of REAL
c₁₄ is ext-real V14() V15() integer set
a . k3 is ext-real V14() V15() Element of REAL
(XFS2FS* a) . k3 is ext-real V14() V15() Element of REAL
b . k3 is ext-real V14() V15() Element of REAL
(XFS2FS* b) . k3 is ext-real V14() V15() Element of REAL
c . k3 is ext-real V14() V15() Element of REAL
(a . k3) + (b . k3) is ext-real V14() V15() Element of REAL
b is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
b . 0 is ext-real V14() V15() Element of REAL
a is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len a is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len b is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
a . 0 is ext-real V14() V15() Element of REAL
XFS2FS* a is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
XFS2FS* b is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
(XFS2FS* a) - (XFS2FS* b) is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Fa is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
Fa - Fb is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len (XFS2FS* a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
len (XFS2FS* b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
c2 is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
len c2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c2 is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
Seg (len (XFS2FS* b)) is V42() V49( len (XFS2FS* b)) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom ((XFS2FS* a) - (XFS2FS* b)) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
dom (XFS2FS* b) is V65() V66() V67() V68() V69() V70() Element of K11(NAT)
Seg (len c2) is V42() V49( len c2) V65() V66() V67() V68() V69() V70() Element of K11(NAT)
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
Replace (p,0,(b . 0)) is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
p2 is T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . c is ext-real V14() V15() Element of REAL
a . c is ext-real V14() V15() Element of REAL
b . c is ext-real V14() V15() Element of REAL
(a . c) - (b . c) is ext-real V14() V15() Element of REAL
(XFS2FS* a) . c is ext-real V14() V15() Element of REAL
(XFS2FS* b) . c is ext-real V14() V15() Element of REAL
((XFS2FS* a) - (XFS2FS* b)) . c is ext-real V14() V15() Element of REAL
p . c is ext-real V14() V15() Element of REAL
c2 . c is ext-real V14() V15() Element of REAL
len p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
p2 . 0 is ext-real V14() V15() Element of REAL
c is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like V42() V53() complex-yielding V55() V56() set
XFS2FS* c is Relation-like NAT -defined REAL -valued Function-like V42() FinSequence-like FinSubsequence-like complex-yielding V55() V56() FinSequence of REAL
c . 0 is ext-real V14() V15() Element of REAL
n is ext-real V14() V15() integer set
len c is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
dom c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
len (XFS2FS* c) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() V64() V65() V66() V67() V68() V69() V70() Element of NAT
p3 is ext-real V14() V15() integer set
p3 is ext-real V14() V15() integer set
k3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V42() V47() set
(XFS2FS* c) . k3 is ext-real V14() V15() Element of REAL
c2 . k3 is ext-real V14() V15() Element of REAL
c₁₄ is ext-real V14() V15() integer set
a . k3 is ext-real V14() V15() Element of REAL
(XFS2FS* a) . k3 is ext-real V14() V15() Element of REAL
b . k3 is ext-real V14() V15() Element of REAL
(XFS2FS* b) . k3 is ext-real V14() V15() Element of REAL
c . k3 is ext-real V14() V15() Element of REAL
(a . k3) - (b . k3) is ext-real V14() V15() Element of REAL