:: O_RING_1 semantic presentation

K88() is set
K92() is V11() V21() V22() V23() M2(K19(K88()))
K19(K88()) is set
K87() is V11() V21() V22() V23() set
K19(K87()) is set
K19(K92()) is set
0 is set
1 is V11() V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
2 is V11() V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
3 is V11() V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
0 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
dom x is M2(K19(K92()))
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
dom y is M2(K19(K92()))
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + (len f) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
Seg ((len y) + (len f)) is V29() V36((len y) + (len f)) M2(K19(K92()))
dom f is M2(K19(K92()))
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
x /. g is M2( the U1 of R)
y /. g is M2( the U1 of R)
x . g is set
y . g is set
g is V21() V22() V23() V27() V28() ext-real V103() set
(len y) + g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. ((len y) + g) is M2( the U1 of R)
f /. g is M2( the U1 of R)
0 + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x . ((len y) + g) is set
f . g is set
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
(len y) + g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x . ((len y) + g) is set
f . g is set
0 + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. ((len y) + g) is M2( the U1 of R)
f /. g is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
x . g is set
y . g is set
x /. g is M2( the U1 of R)
y /. g is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. 1 is M2( the U1 of R)
dom y is M2(K19(K92()))
y . 1 is set
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*x*>) /. ((len y) + 1) is M2( the U1 of R)
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + (len <*x*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (y ^ <*x*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
dom (y ^ <*x*>) is M2(K19(K92()))
(y ^ <*x*>) . ((len y) + 1) is set
R is V21() V22() V23() V27() V28() ext-real V103() set
x is non empty doubleLoopStr
the U1 of x is V11() set
y is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. R is M2( the U1 of x)
f is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
y ^ f is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
(y ^ f) /. R is M2( the U1 of x)
0 + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
dom y is M2(K19(K92()))
R is V21() V22() V23() V27() V28() ext-real V103() set
x is non empty doubleLoopStr
the U1 of x is V11() set
y is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. R is M2( the U1 of x)
f is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
f ^ y is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + R is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(f ^ y) /. ((len f) + R) is M2( the U1 of x)
0 + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
dom y is M2(K19(K92()))
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
x * x is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (y + 1) is M2( the U1 of R)
<*x*> /. y is M2( the U1 of R)
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (y + 1) is M2( the U1 of R)
<*x*> /. y is M2( the U1 of R)
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (y + 1) is M2( the U1 of R)
<*x*> /. y is M2( the U1 of R)
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (y + 1) is M2( the U1 of R)
<*x*> /. y is M2( the U1 of R)
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x /. 1 is M2( the U1 of R)
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. (y + 1) is M2( the U1 of R)
x /. y is M2( the U1 of R)
f is M2( the U1 of R)
(x /. y) + f is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
<*x*> /. 1 is M2( the U1 of R)
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
<*x*> /. y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
<*x*> /. 1 is M2( the U1 of R)
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
<*x*> /. y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (y + 1) is M2( the U1 of R)
<*x*> /. y is M2( the U1 of R)
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x /. 1 is M2( the U1 of R)
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. (y + 1) is M2( the U1 of R)
x /. y is M2( the U1 of R)
f is M2( the U1 of R)
(x /. y) + f is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (y + 1) is M2( the U1 of R)
<*x*> /. y is M2( the U1 of R)
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x /. 1 is M2( the U1 of R)
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. (y + 1) is M2( the U1 of R)
x /. y is M2( the U1 of R)
f is M2( the U1 of R)
(x /. y) + f is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (y + 1) is M2( the U1 of R)
<*x*> /. y is M2( the U1 of R)
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
<*x*> /. 1 is M2( the U1 of R)
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
<*x*> /. y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. 1 is M2( the U1 of R)
R is V21() V22() V23() V27() V28() ext-real V103() set
x is V21() V22() V23() V27() V28() ext-real V103() set
y is non empty doubleLoopStr
the U1 of y is V11() set
f is V1() V4(K92()) V5( the U1 of y) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. R is M2( the U1 of y)
f /. x is M2( the U1 of y)
(f /. R) + (f /. x) is M2( the U1 of y)
<*((f /. R) + (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of y
f ^ <*((f /. R) + (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len (f ^ <*((f /. R) + (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. R) + (f /. x))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*((f /. R) + (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
h is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. h is M2( the U1 of y)
f /. h is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
f /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
f /. m is M2( the U1 of y)
(f /. k) * (f /. m) is M2( the U1 of y)
(f /. k) + (f /. m) is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. k is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. m is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) * ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) + ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. R is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. R) + (f /. x) is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. x is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. R) + ((f ^ <*((f /. R) + (f /. x))*>) /. x) is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) * ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) + ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x ^ y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len (x ^ y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. f is M2( the U1 of R)
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len x) + (len y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
(len x) + g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
y /. h is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
y /. k is M2( the U1 of R)
(y /. h) * (y /. k) is M2( the U1 of R)
(y /. h) + (y /. k) is M2( the U1 of R)
(len x) + h is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len x) + k is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(x ^ y) /. ((len x) + h) is M2( the U1 of R)
(x ^ y) /. ((len x) + k) is M2( the U1 of R)
((x ^ y) /. ((len x) + h)) * ((x ^ y) /. ((len x) + k)) is M2( the U1 of R)
((x ^ y) /. ((len x) + h)) + ((x ^ y) /. ((len x) + k)) is M2( the U1 of R)
((x ^ y) /. ((len x) + h)) + (y /. k) is M2( the U1 of R)
((x ^ y) /. ((len x) + h)) * (y /. k) is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. h is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. k is M2( the U1 of R)
((x ^ y) /. h) * ((x ^ y) /. k) is M2( the U1 of R)
((x ^ y) /. h) + ((x ^ y) /. k) is M2( the U1 of R)
m is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. m is M2( the U1 of R)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. c₉ is M2( the U1 of R)
((x ^ y) /. m) * ((x ^ y) /. c₉) is M2( the U1 of R)
((x ^ y) /. m) + ((x ^ y) /. c₉) is M2( the U1 of R)
x /. f is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
x /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
x /. h is M2( the U1 of R)
(x /. g) * (x /. h) is M2( the U1 of R)
(x /. g) + (x /. h) is M2( the U1 of R)
(x ^ y) /. g is M2( the U1 of R)
(x ^ y) /. h is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. h is M2( the U1 of R)
((x ^ y) /. g) * ((x ^ y) /. h) is M2( the U1 of R)
((x ^ y) /. g) + ((x ^ y) /. h) is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. k is M2( the U1 of R)
m is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. m is M2( the U1 of R)
((x ^ y) /. k) * ((x ^ y) /. m) is M2( the U1 of R)
((x ^ y) /. k) + ((x ^ y) /. m) is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. h is M2( the U1 of R)
((x ^ y) /. g) * ((x ^ y) /. h) is M2( the U1 of R)
((x ^ y) /. g) + ((x ^ y) /. h) is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. k is M2( the U1 of R)
m is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. m is M2( the U1 of R)
((x ^ y) /. k) * ((x ^ y) /. m) is M2( the U1 of R)
((x ^ y) /. k) + ((x ^ y) /. m) is M2( the U1 of R)
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len x) + (len y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) + x is M2( the U1 of R)
<*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(y ^ <*x*>) ^ <*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (y ^ <*x*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*x*>) /. ((len y) + 1) is M2( the U1 of R)
(y ^ <*x*>) /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f /. (len f)) + y is M2( the U1 of R)
<*((f /. (len f)) + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f ^ <*y*>) ^ <*((f /. (len f)) + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len (f ^ <*y*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. (len f)) + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + (len <*((f /. (len f)) + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is V21() V22() V23() V27() V28() ext-real V103() set
x is non empty doubleLoopStr
the U1 of x is V11() set
y is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. R is M2( the U1 of x)
f is V21() V22() V23() V27() V28() ext-real V103() set
y /. f is M2( the U1 of x)
f + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (f + 1) is M2( the U1 of x)
g is M2( the U1 of x)
(y /. f) + g is M2( the U1 of x)
y /. 0 is M2( the U1 of x)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
x /. y is M2( the U1 of R)
f is V21() V22() V23() V27() V28() ext-real V103() set
x /. f is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
x /. g is M2( the U1 of R)
(x /. f) * (x /. g) is M2( the U1 of R)
f is V21() V22() V23() V27() V28() ext-real V103() set
x /. f is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
x /. g is M2( the U1 of R)
(x /. f) * (x /. g) is M2( the U1 of R)
(x /. f) + (x /. g) is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
x /. h is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
x /. k is M2( the U1 of R)
(x /. h) * (x /. k) is M2( the U1 of R)
(x /. h) + (x /. k) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f is V21() V22() V23() V27() V28() ext-real V103() set
<*x*> /. f is M2( the U1 of R)
1 + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) + x is M2( the U1 of R)
<*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(y ^ <*x*>) ^ <*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (y ^ <*x*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*x*>) /. ((len y) + 1) is M2( the U1 of R)
(y ^ <*x*>) /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f /. (len f)) + y is M2( the U1 of R)
<*((f /. (len f)) + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f ^ <*y*>) ^ <*((f /. (len f)) + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len (f ^ <*y*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. (len f)) + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + (len <*((f /. (len f)) + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y is V21() V22() V23() V27() V28() ext-real V103() set
x /. y is M2( the U1 of R)
y + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. (y + 1) is M2( the U1 of R)
f is M2( the U1 of R)
(x /. y) + f is M2( the U1 of R)
x /. 0 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is V21() V22() V23() V27() V28() ext-real V103() set
x is V21() V22() V23() V27() V28() ext-real V103() set
y is non empty doubleLoopStr
the U1 of y is V11() set
f is V1() V4(K92()) V5( the U1 of y) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. R is M2( the U1 of y)
f /. x is M2( the U1 of y)
(f /. R) * (f /. x) is M2( the U1 of y)
<*((f /. R) * (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of y
f ^ <*((f /. R) * (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len (f ^ <*((f /. R) * (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. R) * (f /. x))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*((f /. R) * (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
h is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. h is M2( the U1 of y)
f /. h is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
f /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
f /. m is M2( the U1 of y)
(f /. k) * (f /. m) is M2( the U1 of y)
(f /. k) + (f /. m) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) + ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. R is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. R) * (f /. x) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. x is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. R) * ((f ^ <*((f /. R) * (f /. x))*>) /. x) is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) + ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) * x is M2( the U1 of R)
<*((y /. (len y)) * x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(y ^ <*x*>) ^ <*((y /. (len y)) * x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (y ^ <*x*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*x*>) /. ((len y) + 1) is M2( the U1 of R)
(y ^ <*x*>) /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f /. (len f)) * y is M2( the U1 of R)
<*((f /. (len f)) * y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f ^ <*y*>) ^ <*((f /. (len f)) * y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len (f ^ <*y*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. (len f)) * y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + (len <*((f /. (len f)) * y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is V21() V22() V23() V27() V28() ext-real V103() set
x is non empty doubleLoopStr
the U1 of x is V11() set
y is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. R is M2( the U1 of x)
f is V21() V22() V23() V27() V28() ext-real V103() set
y /. f is M2( the U1 of x)
f + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (f + 1) is M2( the U1 of x)
g is M2( the U1 of x)
(y /. f) * g is M2( the U1 of x)
y /. 0 is M2( the U1 of x)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f is V21() V22() V23() V27() V28() ext-real V103() set
<*x*> /. f is M2( the U1 of R)
1 + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) + x is M2( the U1 of R)
<*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(y ^ <*x*>) ^ <*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (y ^ <*x*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*x*>) /. ((len y) + 1) is M2( the U1 of R)
(y ^ <*x*>) /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*y*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f /. (len f)) + y is M2( the U1 of R)
<*((f /. (len f)) + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f ^ <*y*>) ^ <*((f /. (len f)) + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len (f ^ <*y*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. (len f)) + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + (len <*((f /. (len f)) + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ <*y*>)) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is V21() V22() V23() V27() V28() ext-real V103() set
x is non empty doubleLoopStr
the U1 of x is V11() set
y is V1() V4(K92()) V5( the U1 of x) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of x
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. R is M2( the U1 of x)
f is V21() V22() V23() V27() V28() ext-real V103() set
y /. f is M2( the U1 of x)
f + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (f + 1) is M2( the U1 of x)
g is M2( the U1 of x)
(y /. f) + g is M2( the U1 of x)
y /. 0 is M2( the U1 of x)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) + x is M2( the U1 of R)
<*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len (y ^ <*((y /. (len y)) + x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((y /. (len y)) + x)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + (len <*((y /. (len y)) + x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
y /. g is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. g is M2( the U1 of R)
dom y is M2(K19(K92()))
g is V21() V22() V23() V27() V28() ext-real V103() set
g + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*((y /. (len y)) + x)*>) /. (g + 1) is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. g is M2( the U1 of R)
y /. g is M2( the U1 of R)
y /. (g + 1) is M2( the U1 of R)
dom y is M2(K19(K92()))
(y /. g) + x is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + x is M2( the U1 of R)
h is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + h is M2( the U1 of R)
k is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + k is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. 1 is M2( the U1 of R)
y /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) + x is M2( the U1 of R)
<*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len (y ^ <*((y /. (len y)) + x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((y /. (len y)) + x)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + (len <*((y /. (len y)) + x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
y /. g is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. g is M2( the U1 of R)
dom y is M2(K19(K92()))
g is V21() V22() V23() V27() V28() ext-real V103() set
g + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*((y /. (len y)) + x)*>) /. (g + 1) is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. g is M2( the U1 of R)
y /. g is M2( the U1 of R)
y /. (g + 1) is M2( the U1 of R)
dom y is M2(K19(K92()))
(y /. g) + x is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + x is M2( the U1 of R)
h is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + h is M2( the U1 of R)
k is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + k is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. 1 is M2( the U1 of R)
y /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) + x is M2( the U1 of R)
<*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*((y /. (len y)) + x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len (y ^ <*((y /. (len y)) + x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((y /. (len y)) + x)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + (len <*((y /. (len y)) + x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
y /. g is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. g is M2( the U1 of R)
dom y is M2(K19(K92()))
g is V21() V22() V23() V27() V28() ext-real V103() set
g + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*((y /. (len y)) + x)*>) /. (g + 1) is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. g is M2( the U1 of R)
y /. g is M2( the U1 of R)
y /. (g + 1) is M2( the U1 of R)
dom y is M2(K19(K92()))
(y /. g) + x is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + x is M2( the U1 of R)
h is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + h is M2( the U1 of R)
k is M2( the U1 of R)
((y ^ <*((y /. (len y)) + x)*>) /. g) + k is M2( the U1 of R)
(y ^ <*((y /. (len y)) + x)*>) /. 1 is M2( the U1 of R)
y /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is V21() V22() V23() V27() V28() ext-real V103() set
x is V21() V22() V23() V27() V28() ext-real V103() set
y is non empty doubleLoopStr
the U1 of y is V11() set
f is V1() V4(K92()) V5( the U1 of y) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. R is M2( the U1 of y)
f /. x is M2( the U1 of y)
(f /. R) + (f /. x) is M2( the U1 of y)
<*((f /. R) + (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of y
f ^ <*((f /. R) + (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len (f ^ <*((f /. R) + (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. R) + (f /. x))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*((f /. R) + (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
h is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. h is M2( the U1 of y)
f /. h is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
f /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
f /. m is M2( the U1 of y)
(f /. k) * (f /. m) is M2( the U1 of y)
(f /. k) + (f /. m) is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. k is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. m is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) * ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) + ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. R is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. R) + (f /. x) is M2( the U1 of y)
(f ^ <*((f /. R) + (f /. x))*>) /. x is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. R) + ((f ^ <*((f /. R) + (f /. x))*>) /. x) is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) * ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. k) + ((f ^ <*((f /. R) + (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) + (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) + (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) + (f /. x))*>) /. c₁₀) is M2( the U1 of y)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
1 + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
<*x*> ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
len <*x*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
<*x*> /. (len <*x*>) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len <*x*>) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len <*x*>) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. (len x) is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x ^ y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(x /. (len x)) + (y /. (len y)) is M2( the U1 of R)
<*((x /. (len x)) + (y /. (len y)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(x ^ y) ^ <*((x /. (len x)) + (y /. (len y)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(len x) + (len y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
dom x is M2(K19(K92()))
len (x ^ y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(x ^ y) /. (len x) is M2( the U1 of R)
dom y is M2(K19(K92()))
(x ^ y) /. ((len x) + (len y)) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
g is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
f ^ g is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f /. (len f)) + (g /. (len g)) is M2( the U1 of R)
<*((f /. (len f)) + (g /. (len g)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len ((f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (f ^ g) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. (len f)) + (g /. (len g)))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ g)) + (len <*((f /. (len f)) + (g /. (len g)))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ g)) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
((f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*>) /. (len ((f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*>)) is M2( the U1 of R)
x + (g /. (len g)) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x + y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x + y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x + y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x + y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x ^ y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len (x ^ y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. f is M2( the U1 of R)
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len x) + (len y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
(len x) + g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
y /. h is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
y /. k is M2( the U1 of R)
(y /. h) * (y /. k) is M2( the U1 of R)
(len x) + h is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len x) + k is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(x ^ y) /. ((len x) + h) is M2( the U1 of R)
((x ^ y) /. ((len x) + h)) * (y /. k) is M2( the U1 of R)
(x ^ y) /. ((len x) + k) is M2( the U1 of R)
((x ^ y) /. ((len x) + h)) * ((x ^ y) /. ((len x) + k)) is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. h is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. k is M2( the U1 of R)
((x ^ y) /. h) * ((x ^ y) /. k) is M2( the U1 of R)
m is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. m is M2( the U1 of R)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. c₉ is M2( the U1 of R)
((x ^ y) /. m) * ((x ^ y) /. c₉) is M2( the U1 of R)
x /. f is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
x /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
x /. h is M2( the U1 of R)
(x /. g) * (x /. h) is M2( the U1 of R)
(x ^ y) /. g is M2( the U1 of R)
((x ^ y) /. g) * (x /. h) is M2( the U1 of R)
(x ^ y) /. h is M2( the U1 of R)
((x ^ y) /. g) * ((x ^ y) /. h) is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. h is M2( the U1 of R)
((x ^ y) /. g) * ((x ^ y) /. h) is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. k is M2( the U1 of R)
m is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. m is M2( the U1 of R)
((x ^ y) /. k) * ((x ^ y) /. m) is M2( the U1 of R)
g is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. g is M2( the U1 of R)
h is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. h is M2( the U1 of R)
((x ^ y) /. g) * ((x ^ y) /. h) is M2( the U1 of R)
k is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. k is M2( the U1 of R)
m is V21() V22() V23() V27() V28() ext-real V103() set
(x ^ y) /. m is M2( the U1 of R)
((x ^ y) /. k) * ((x ^ y) /. m) is M2( the U1 of R)
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len x) + (len y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is V21() V22() V23() V27() V28() ext-real V103() set
x is V21() V22() V23() V27() V28() ext-real V103() set
y is non empty doubleLoopStr
the U1 of y is V11() set
f is V1() V4(K92()) V5( the U1 of y) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. R is M2( the U1 of y)
f /. x is M2( the U1 of y)
(f /. R) * (f /. x) is M2( the U1 of y)
<*((f /. R) * (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of y
f ^ <*((f /. R) * (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len (f ^ <*((f /. R) * (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. R) * (f /. x))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*((f /. R) * (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
h is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. h is M2( the U1 of y)
f /. h is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
f /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
f /. m is M2( the U1 of y)
(f /. k) * (f /. m) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * (f /. m) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. R is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. R) * (f /. x) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. x is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. R) * ((f ^ <*((f /. R) * (f /. x))*>) /. x) is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
R is V21() V22() V23() V27() V28() ext-real V103() set
x is V21() V22() V23() V27() V28() ext-real V103() set
y is non empty doubleLoopStr
the U1 of y is V11() set
f is V1() V4(K92()) V5( the U1 of y) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. R is M2( the U1 of y)
f /. x is M2( the U1 of y)
(f /. R) * (f /. x) is M2( the U1 of y)
<*((f /. R) * (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of y
f ^ <*((f /. R) * (f /. x))*> is V1() V4(K92()) V5( the U1 of y) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of y
len (f ^ <*((f /. R) * (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. R) * (f /. x))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*((f /. R) * (f /. x))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
h is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. h is M2( the U1 of y)
f /. h is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
f /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
f /. m is M2( the U1 of y)
(f /. k) * (f /. m) is M2( the U1 of y)
(f /. k) + (f /. m) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) + ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. R is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. R) * (f /. x) is M2( the U1 of y)
(f ^ <*((f /. R) * (f /. x))*>) /. x is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. R) * ((f ^ <*((f /. R) * (f /. x))*>) /. x) is M2( the U1 of y)
k is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. k is M2( the U1 of y)
m is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. m is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) * ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. k) + ((f ^ <*((f /. R) * (f /. x))*>) /. m) is M2( the U1 of y)
c₉ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₉ is M2( the U1 of y)
c₁₀ is V21() V22() V23() V27() V28() ext-real V103() set
(f ^ <*((f /. R) * (f /. x))*>) /. c₁₀ is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) * ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
((f ^ <*((f /. R) * (f /. x))*>) /. c₉) + ((f ^ <*((f /. R) * (f /. x))*>) /. c₁₀) is M2( the U1 of y)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(y /. (len y)) * x is M2( the U1 of R)
<*((y /. (len y)) * x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
y ^ <*((y /. (len y)) * x)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len (y ^ <*((y /. (len y)) * x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((y /. (len y)) * x)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + (len <*((y /. (len y)) * x)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len y) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g is V21() V22() V23() V27() V28() ext-real V103() set
y /. g is M2( the U1 of R)
(y ^ <*((y /. (len y)) * x)*>) /. g is M2( the U1 of R)
dom y is M2(K19(K92()))
g is V21() V22() V23() V27() V28() ext-real V103() set
g + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(y ^ <*((y /. (len y)) * x)*>) /. (g + 1) is M2( the U1 of R)
(y ^ <*((y /. (len y)) * x)*>) /. g is M2( the U1 of R)
y /. g is M2( the U1 of R)
y /. (g + 1) is M2( the U1 of R)
dom y is M2(K19(K92()))
(y /. g) * x is M2( the U1 of R)
((y ^ <*((y /. (len y)) * x)*>) /. g) * x is M2( the U1 of R)
h is M2( the U1 of R)
((y ^ <*((y /. (len y)) * x)*>) /. g) * h is M2( the U1 of R)
k is M2( the U1 of R)
((y ^ <*((y /. (len y)) * x)*>) /. g) * k is M2( the U1 of R)
(y ^ <*((y /. (len y)) * x)*>) /. 1 is M2( the U1 of R)
y /. 1 is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. (len x) is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x ^ y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(x /. (len x)) * (y /. (len y)) is M2( the U1 of R)
<*((x /. (len x)) * (y /. (len y)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(x ^ y) ^ <*((x /. (len x)) * (y /. (len y)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(len x) + (len y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (x ^ y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(x ^ y) /. (len x) is M2( the U1 of R)
(x ^ y) /. ((len x) + (len y)) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len x is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
x /. (len x) is M2( the U1 of R)
y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
x ^ y is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len y is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
y /. (len y) is M2( the U1 of R)
(x /. (len x)) * (y /. (len y)) is M2( the U1 of R)
<*((x /. (len x)) * (y /. (len y)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(x ^ y) ^ <*((x /. (len x)) * (y /. (len y)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(len x) + (len y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
dom x is M2(K19(K92()))
len (x ^ y) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(x ^ y) /. (len x) is M2( the U1 of R)
dom y is M2(K19(K92()))
(x ^ y) /. ((len x) + (len y)) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x * y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x * y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x * y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x * y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
<*(x * y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
f ^ <*(x * y)*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
g is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
len <*(x * y)*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + (len <*(x * y)*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len f) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
g is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
f ^ g is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f /. (len f)) * (g /. (len g)) is M2( the U1 of R)
<*((f /. (len f)) * (g /. (len g)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
h is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len h is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
h /. (len h) is M2( the U1 of R)
len (f ^ g) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. (len f)) * (g /. (len g)))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ g)) + (len <*((f /. (len f)) * (g /. (len g)))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ g)) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
f is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len f is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
f /. (len f) is M2( the U1 of R)
g is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len g is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
g /. (len g) is M2( the U1 of R)
f ^ g is V1() V4(K92()) V5( the U1 of R) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f /. (len f)) * (g /. (len g)) is M2( the U1 of R)
<*((f /. (len f)) * (g /. (len g)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of the U1 of R
(f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is V1() V4(K92()) V5( the U1 of R) Function-like V11() V29() FinSequence-like FinSubsequence-like FinSequence of the U1 of R
len ((f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len (f ^ g) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
len <*((f /. (len f)) * (g /. (len g)))*> is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ g)) + (len <*((f /. (len f)) * (g /. (len g)))*>) is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
(len (f ^ g)) + 1 is V21() V22() V23() V27() V28() ext-real V103() M3(K88(),K92())
((f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>) /. (len ((f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>)) is M2( the U1 of R)
x * (g /. (len g)) is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)
R is non empty doubleLoopStr
the U1 of R is V11() set
x is M2( the U1 of R)
y is M2( the U1 of R)
x * y is M2( the U1 of R)