:: SERIES_4 semantic presentation

REAL is V4() V46() V57() V58() V59() V63() set
NAT is V57() V58() V59() V60() V61() V62() V63() Element of K11(REAL)
K11(REAL) is set
COMPLEX is V4() V46() V57() V63() set
RAT is V4() V46() V57() V58() V59() V60() V63() set
INT is V4() V46() V57() V58() V59() V60() V61() V63() set
K12(COMPLEX,COMPLEX) is V35() set
K11(K12(COMPLEX,COMPLEX)) is set
K12(K12(COMPLEX,COMPLEX),COMPLEX) is V35() set
K11(K12(K12(COMPLEX,COMPLEX),COMPLEX)) is set
K12(REAL,REAL) is V35() V36() V37() set
K11(K12(REAL,REAL)) is set
K12(K12(REAL,REAL),REAL) is V35() V36() V37() set
K11(K12(K12(REAL,REAL),REAL)) is set
K12(RAT,RAT) is V20( RAT ) V35() V36() V37() set
K11(K12(RAT,RAT)) is set
K12(K12(RAT,RAT),RAT) is V20( RAT ) V35() V36() V37() set
K11(K12(K12(RAT,RAT),RAT)) is set
K12(INT,INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K11(K12(INT,INT)) is set
K12(K12(INT,INT),INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K11(K12(K12(INT,INT),INT)) is set
K12(NAT,NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K12(K12(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K11(K12(K12(NAT,NAT),NAT)) is set
NAT is V57() V58() V59() V60() V61() V62() V63() set
K11(NAT) is set
K11(NAT) is set
K12(NAT,REAL) is V35() V36() V37() set
K11(K12(NAT,REAL)) is set
0 is ext-real non positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() V63() Element of NAT
1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
1 ! is ext-real positive non negative V4() ordinal natural V14() real Element of REAL
2 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
2 ! is ext-real positive non negative V4() ordinal natural V14() real Element of REAL
4 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
2 |^ 2 is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
s is ext-real V14() real set
s |^ 2 is ext-real V14() real set
2 * s is ext-real V14() real set
n is ext-real V14() real set
s + n is ext-real V14() real set
(s + n) |^ 2 is ext-real V14() real set
(2 * s) * n is ext-real V14() real set
(s |^ 2) + ((2 * s) * n) is ext-real V14() real set
n |^ 2 is ext-real V14() real set
((s |^ 2) + ((2 * s) * n)) + (n |^ 2) is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(s + n) |^ (1 + 1) is ext-real V14() real set
(s + n) |^ 1 is ext-real V14() real set
((s + n) |^ 1) * (s + n) is ext-real V14() real set
(s + n) * (s + n) is ext-real V14() real set
s * s is ext-real V14() real set
s * n is ext-real V14() real set
(s * s) + (s * n) is ext-real V14() real set
n * n is ext-real V14() real set
(s * n) + (n * n) is ext-real V14() real set
((s * s) + (s * n)) + ((s * n) + (n * n)) is ext-real V14() real set
(s * n) + (n |^ 2) is ext-real V14() real set
((s * s) + (s * n)) + ((s * n) + (n |^ 2)) is ext-real V14() real set
(s |^ 2) + (s * n) is ext-real V14() real set
((s |^ 2) + (s * n)) + ((s * n) + (n |^ 2)) is ext-real V14() real set
2 * (s * n) is ext-real V14() real set
(s |^ 2) + (2 * (s * n)) is ext-real V14() real set
((s |^ 2) + (2 * (s * n))) + (n |^ 2) is ext-real V14() real set
2 * 2 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
1 / 2 is ext-real positive non negative V4() V14() real set
1 / 4 is ext-real positive non negative V4() V14() real set
s is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
s + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(1 / 2) |^ (s + 1) is ext-real V14() real set
2 |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((1 / 2) |^ (s + 1)) + (2 |^ (s + 1)) is ext-real V14() real set
(((1 / 2) |^ (s + 1)) + (2 |^ (s + 1))) |^ 2 is ext-real V14() real set
(1 / 4) |^ (s + 1) is ext-real V14() real set
4 |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((1 / 4) |^ (s + 1)) + (4 |^ (s + 1)) is ext-real V14() real set
(((1 / 4) |^ (s + 1)) + (4 |^ (s + 1))) + 2 is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(((1 / 2) |^ (s + 1)) + (2 |^ (s + 1))) |^ (1 + 1) is ext-real V14() real set
(((1 / 2) |^ (s + 1)) + (2 |^ (s + 1))) |^ 1 is ext-real V14() real set
((((1 / 2) |^ (s + 1)) + (2 |^ (s + 1))) |^ 1) * (((1 / 2) |^ (s + 1)) + (2 |^ (s + 1))) is ext-real V14() real set
(((1 / 2) |^ (s + 1)) + (2 |^ (s + 1))) * (((1 / 2) |^ (s + 1)) + (2 |^ (s + 1))) is ext-real V14() real set
((1 / 2) |^ (s + 1)) * ((1 / 2) |^ (s + 1)) is ext-real V14() real set
((1 / 2) |^ (s + 1)) * (2 |^ (s + 1)) is ext-real V14() real set
(((1 / 2) |^ (s + 1)) * ((1 / 2) |^ (s + 1))) + (((1 / 2) |^ (s + 1)) * (2 |^ (s + 1))) is ext-real V14() real set
(2 |^ (s + 1)) * ((1 / 2) |^ (s + 1)) is ext-real V14() real set
(2 |^ (s + 1)) * (2 |^ (s + 1)) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((2 |^ (s + 1)) * ((1 / 2) |^ (s + 1))) + ((2 |^ (s + 1)) * (2 |^ (s + 1))) is ext-real V14() real set
((((1 / 2) |^ (s + 1)) * ((1 / 2) |^ (s + 1))) + (((1 / 2) |^ (s + 1)) * (2 |^ (s + 1)))) + (((2 |^ (s + 1)) * ((1 / 2) |^ (s + 1))) + ((2 |^ (s + 1)) * (2 |^ (s + 1)))) is ext-real V14() real set
(1 / 2) * (1 / 2) is ext-real positive non negative V4() V14() real set
((1 / 2) * (1 / 2)) |^ (s + 1) is ext-real V14() real set
(((1 / 2) * (1 / 2)) |^ (s + 1)) + (((1 / 2) |^ (s + 1)) * (2 |^ (s + 1))) is ext-real V14() real set
((((1 / 2) * (1 / 2)) |^ (s + 1)) + (((1 / 2) |^ (s + 1)) * (2 |^ (s + 1)))) + (((2 |^ (s + 1)) * ((1 / 2) |^ (s + 1))) + ((2 |^ (s + 1)) * (2 |^ (s + 1)))) is ext-real V14() real set
(1 / 2) * 1 is ext-real positive non negative V4() V14() real set
((1 / 2) * 1) / 2 is ext-real positive non negative V4() V14() real set
(((1 / 2) * 1) / 2) |^ (s + 1) is ext-real V14() real set
(1 / 2) * 2 is ext-real positive non negative V4() V14() real set
((1 / 2) * 2) |^ (s + 1) is ext-real V14() real set
((((1 / 2) * 1) / 2) |^ (s + 1)) + (((1 / 2) * 2) |^ (s + 1)) is ext-real V14() real set
(((((1 / 2) * 1) / 2) |^ (s + 1)) + (((1 / 2) * 2) |^ (s + 1))) + (((2 |^ (s + 1)) * ((1 / 2) |^ (s + 1))) + ((2 |^ (s + 1)) * (2 |^ (s + 1)))) is ext-real V14() real set
2 * (1 / 2) is ext-real positive non negative V4() V14() real set
(2 * (1 / 2)) |^ (s + 1) is ext-real V14() real set
((2 * (1 / 2)) |^ (s + 1)) + ((2 |^ (s + 1)) * (2 |^ (s + 1))) is ext-real V14() real set
(((((1 / 2) * 1) / 2) |^ (s + 1)) + (((1 / 2) * 2) |^ (s + 1))) + (((2 * (1 / 2)) |^ (s + 1)) + ((2 |^ (s + 1)) * (2 |^ (s + 1)))) is ext-real V14() real set
2 * 2 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * 2) |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (1 / 2)) |^ (s + 1)) + ((2 * 2) |^ (s + 1)) is ext-real V14() real set
(((((1 / 2) * 1) / 2) |^ (s + 1)) + (((1 / 2) * 2) |^ (s + 1))) + (((2 * (1 / 2)) |^ (s + 1)) + ((2 * 2) |^ (s + 1))) is ext-real V14() real set
((1 / 4) |^ (s + 1)) + 1 is ext-real V14() real set
1 |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(1 |^ (s + 1)) + (4 |^ (s + 1)) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(((1 / 4) |^ (s + 1)) + 1) + ((1 |^ (s + 1)) + (4 |^ (s + 1))) is ext-real V14() real set
1 + (4 |^ (s + 1)) is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(((1 / 4) |^ (s + 1)) + 1) + (1 + (4 |^ (s + 1))) is ext-real V14() real set
((1 / 4) |^ (s + 1)) + 2 is ext-real V14() real set
(((1 / 4) |^ (s + 1)) + 2) + (4 |^ (s + 1)) is ext-real V14() real set
3 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
1 / 3 is ext-real positive non negative V4() V14() real set
9 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
1 / 9 is ext-real positive non negative V4() V14() real set
s is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
s + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(1 / 3) |^ (s + 1) is ext-real V14() real set
3 |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((1 / 3) |^ (s + 1)) + (3 |^ (s + 1)) is ext-real V14() real set
(((1 / 3) |^ (s + 1)) + (3 |^ (s + 1))) |^ 2 is ext-real V14() real set
(1 / 9) |^ (s + 1) is ext-real V14() real set
9 |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((1 / 9) |^ (s + 1)) + (9 |^ (s + 1)) is ext-real V14() real set
(((1 / 9) |^ (s + 1)) + (9 |^ (s + 1))) + 2 is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(((1 / 3) |^ (s + 1)) + (3 |^ (s + 1))) |^ (1 + 1) is ext-real V14() real set
(((1 / 3) |^ (s + 1)) + (3 |^ (s + 1))) |^ 1 is ext-real V14() real set
((((1 / 3) |^ (s + 1)) + (3 |^ (s + 1))) |^ 1) * (((1 / 3) |^ (s + 1)) + (3 |^ (s + 1))) is ext-real V14() real set
(((1 / 3) |^ (s + 1)) + (3 |^ (s + 1))) * (((1 / 3) |^ (s + 1)) + (3 |^ (s + 1))) is ext-real V14() real set
((1 / 3) |^ (s + 1)) * ((1 / 3) |^ (s + 1)) is ext-real V14() real set
((1 / 3) |^ (s + 1)) * (3 |^ (s + 1)) is ext-real V14() real set
(((1 / 3) |^ (s + 1)) * ((1 / 3) |^ (s + 1))) + (((1 / 3) |^ (s + 1)) * (3 |^ (s + 1))) is ext-real V14() real set
(3 |^ (s + 1)) * ((1 / 3) |^ (s + 1)) is ext-real V14() real set
(3 |^ (s + 1)) * (3 |^ (s + 1)) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((3 |^ (s + 1)) * ((1 / 3) |^ (s + 1))) + ((3 |^ (s + 1)) * (3 |^ (s + 1))) is ext-real V14() real set
((((1 / 3) |^ (s + 1)) * ((1 / 3) |^ (s + 1))) + (((1 / 3) |^ (s + 1)) * (3 |^ (s + 1)))) + (((3 |^ (s + 1)) * ((1 / 3) |^ (s + 1))) + ((3 |^ (s + 1)) * (3 |^ (s + 1)))) is ext-real V14() real set
(1 / 3) * (1 / 3) is ext-real positive non negative V4() V14() real set
((1 / 3) * (1 / 3)) |^ (s + 1) is ext-real V14() real set
(((1 / 3) * (1 / 3)) |^ (s + 1)) + (((1 / 3) |^ (s + 1)) * (3 |^ (s + 1))) is ext-real V14() real set
((((1 / 3) * (1 / 3)) |^ (s + 1)) + (((1 / 3) |^ (s + 1)) * (3 |^ (s + 1)))) + (((3 |^ (s + 1)) * ((1 / 3) |^ (s + 1))) + ((3 |^ (s + 1)) * (3 |^ (s + 1)))) is ext-real V14() real set
(1 / 3) * 1 is ext-real positive non negative V4() V14() real set
((1 / 3) * 1) / 3 is ext-real positive non negative V4() V14() real set
(((1 / 3) * 1) / 3) |^ (s + 1) is ext-real V14() real set
(1 / 3) * 3 is ext-real positive non negative V4() V14() real set
((1 / 3) * 3) |^ (s + 1) is ext-real V14() real set
((((1 / 3) * 1) / 3) |^ (s + 1)) + (((1 / 3) * 3) |^ (s + 1)) is ext-real V14() real set
(((((1 / 3) * 1) / 3) |^ (s + 1)) + (((1 / 3) * 3) |^ (s + 1))) + (((3 |^ (s + 1)) * ((1 / 3) |^ (s + 1))) + ((3 |^ (s + 1)) * (3 |^ (s + 1)))) is ext-real V14() real set
3 * (1 / 3) is ext-real positive non negative V4() V14() real set
(3 * (1 / 3)) |^ (s + 1) is ext-real V14() real set
((3 * (1 / 3)) |^ (s + 1)) + ((3 |^ (s + 1)) * (3 |^ (s + 1))) is ext-real V14() real set
(((((1 / 3) * 1) / 3) |^ (s + 1)) + (((1 / 3) * 3) |^ (s + 1))) + (((3 * (1 / 3)) |^ (s + 1)) + ((3 |^ (s + 1)) * (3 |^ (s + 1)))) is ext-real V14() real set
3 * 3 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * 3) |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((3 * (1 / 3)) |^ (s + 1)) + ((3 * 3) |^ (s + 1)) is ext-real V14() real set
(((((1 / 3) * 1) / 3) |^ (s + 1)) + (((1 / 3) * 3) |^ (s + 1))) + (((3 * (1 / 3)) |^ (s + 1)) + ((3 * 3) |^ (s + 1))) is ext-real V14() real set
((1 / 9) |^ (s + 1)) + 1 is ext-real V14() real set
1 |^ (s + 1) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(1 |^ (s + 1)) + (9 |^ (s + 1)) is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(((1 / 9) |^ (s + 1)) + 1) + ((1 |^ (s + 1)) + (9 |^ (s + 1))) is ext-real V14() real set
1 + (9 |^ (s + 1)) is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(((1 / 9) |^ (s + 1)) + 1) + (1 + (9 |^ (s + 1))) is ext-real V14() real set
((1 / 9) |^ (s + 1)) + 2 is ext-real V14() real set
(((1 / 9) |^ (s + 1)) + 2) + (9 |^ (s + 1)) is ext-real V14() real set
s is ext-real V14() real set
s |^ 2 is ext-real V14() real set
n is ext-real V14() real set
s - n is ext-real V14() real set
s + n is ext-real V14() real set
(s - n) * (s + n) is ext-real V14() real set
n |^ 2 is ext-real V14() real set
(s |^ 2) - (n |^ 2) is ext-real V14() real set
s * s is ext-real V14() real set
n * n is ext-real V14() real set
(s * s) - (n * n) is ext-real V14() real set
(s |^ 2) - (n * n) is ext-real V14() real set
s is ext-real V14() real set
s |^ 2 is ext-real V14() real set
2 * s is ext-real V14() real set
n is ext-real V14() real set
s - n is ext-real V14() real set
(s - n) |^ 2 is ext-real V14() real set
(2 * s) * n is ext-real V14() real set
(s |^ 2) - ((2 * s) * n) is ext-real V14() real set
n |^ 2 is ext-real V14() real set
((s |^ 2) - ((2 * s) * n)) + (n |^ 2) is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(s - n) |^ (1 + 1) is ext-real V14() real set
(s - n) |^ 1 is ext-real V14() real set
((s - n) |^ 1) * (s - n) is ext-real V14() real set
(s - n) * (s - n) is ext-real V14() real set
s * s is ext-real V14() real set
s * n is ext-real V14() real set
(s * s) - (s * n) is ext-real V14() real set
n * n is ext-real V14() real set
(s * n) - (n * n) is ext-real V14() real set
((s * s) - (s * n)) - ((s * n) - (n * n)) is ext-real V14() real set
(s * n) - (n |^ 2) is ext-real V14() real set
((s * s) - (s * n)) - ((s * n) - (n |^ 2)) is ext-real V14() real set
(s |^ 2) - (s * n) is ext-real V14() real set
((s |^ 2) - (s * n)) - ((s * n) - (n |^ 2)) is ext-real V14() real set
2 * (s * n) is ext-real V14() real set
(s |^ 2) - (2 * (s * n)) is ext-real V14() real set
((s |^ 2) - (2 * (s * n))) + (n |^ 2) is ext-real V14() real set
s is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
s + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
s + 2 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
n is ext-real V14() real set
n |^ s is ext-real V14() real set
1 - (n |^ s) is ext-real V14() real set
n * (1 - (n |^ s)) is ext-real V14() real set
1 - n is ext-real V14() real set
(1 - n) |^ 2 is ext-real V14() real set
(n * (1 - (n |^ s))) / ((1 - n) |^ 2) is ext-real V14() real set
n |^ (s + 1) is ext-real V14() real set
s * (n |^ (s + 1)) is ext-real V14() real set
(s * (n |^ (s + 1))) / (1 - n) is ext-real V14() real set
((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - ((s * (n |^ (s + 1))) / (1 - n)) is ext-real V14() real set
(((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - ((s * (n |^ (s + 1))) / (1 - n))) + (s * (n |^ (s + 1))) is ext-real V14() real set
((((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - ((s * (n |^ (s + 1))) / (1 - n))) + (s * (n |^ (s + 1)))) + (n |^ (s + 1)) is ext-real V14() real set
1 - (n |^ (s + 1)) is ext-real V14() real set
n * (1 - (n |^ (s + 1))) is ext-real V14() real set
(n * (1 - (n |^ (s + 1)))) / ((1 - n) |^ 2) is ext-real V14() real set
n |^ (s + 2) is ext-real V14() real set
(s + 1) * (n |^ (s + 2)) is ext-real V14() real set
((s + 1) * (n |^ (s + 2))) / (1 - n) is ext-real V14() real set
((n * (1 - (n |^ (s + 1)))) / ((1 - n) |^ 2)) - (((s + 1) * (n |^ (s + 2))) / (1 - n)) is ext-real V14() real set
(1 - n) * (s * (n |^ (s + 1))) is ext-real V14() real set
(1 - n) * (1 - n) is ext-real V14() real set
((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) * (1 - n)) is ext-real V14() real set
((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - (((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) * (1 - n))) is ext-real V14() real set
(((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - (((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) * (1 - n)))) + (s * (n |^ (s + 1))) is ext-real V14() real set
((((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - (((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) * (1 - n)))) + (s * (n |^ (s + 1)))) + (n |^ (s + 1)) is ext-real V14() real set
((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) |^ 2) is ext-real V14() real set
((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - (((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) |^ 2)) is ext-real V14() real set
(((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - (((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) |^ 2))) + (s * (n |^ (s + 1))) is ext-real V14() real set
((((n * (1 - (n |^ s))) / ((1 - n) |^ 2)) - (((1 - n) * (s * (n |^ (s + 1)))) / ((1 - n) |^ 2))) + (s * (n |^ (s + 1)))) + (n |^ (s + 1)) is ext-real V14() real set
n * (n |^ s) is ext-real V14() real set
n - (n * (n |^ s)) is ext-real V14() real set
(s * (n |^ (s + 1))) * n is ext-real V14() real set
(s * (n |^ (s + 1))) - ((s * (n |^ (s + 1))) * n) is ext-real V14() real set
(n - (n * (n |^ s))) - ((s * (n |^ (s + 1))) - ((s * (n |^ (s + 1))) * n)) is ext-real V14() real set
((n - (n * (n |^ s))) - ((s * (n |^ (s + 1))) - ((s * (n |^ (s + 1))) * n))) / ((1 - n) |^ 2) is ext-real V14() real set
(((n - (n * (n |^ s))) - ((s * (n |^ (s + 1))) - ((s * (n |^ (s + 1))) * n))) / ((1 - n) |^ 2)) + (s * (n |^ (s + 1))) is ext-real V14() real set
((((n - (n * (n |^ s))) - ((s * (n |^ (s + 1))) - ((s * (n |^ (s + 1))) * n))) / ((1 - n) |^ 2)) + (s * (n |^ (s + 1)))) + (n |^ (s + 1)) is ext-real V14() real set
(n - (n * (n |^ s))) - (s * (n |^ (s + 1))) is ext-real V14() real set
n * s is ext-real V14() real set
(n * s) * (n |^ (s + 1)) is ext-real V14() real set
((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1))) is ext-real V14() real set
(((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2) is ext-real V14() real set
(s * (n |^ (s + 1))) + (n |^ (s + 1)) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * 1 is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * 1) is ext-real V14() real set
(1 - n) / (1 - n) is ext-real V14() real set
((1 - n) / (1 - n)) * 1 is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) / (1 - n)) * 1) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) / (1 - n)) * 1)) is ext-real V14() real set
((1 - n) / (1 - n)) * ((1 - n) / (1 - n)) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) / (1 - n)) * ((1 - n) / (1 - n))) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) / (1 - n)) * ((1 - n) / (1 - n)))) is ext-real V14() real set
((1 - n) * (1 - n)) / ((1 - n) * (1 - n)) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) * (1 - n)) / ((1 - n) * (1 - n))) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) * (1 - n)) / ((1 - n) * (1 - n)))) is ext-real V14() real set
(1 - n) |^ 1 is ext-real V14() real set
((1 - n) |^ 1) * (1 - n) is ext-real V14() real set
(((1 - n) |^ 1) * (1 - n)) / ((1 - n) * (1 - n)) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((((1 - n) |^ 1) * (1 - n)) / ((1 - n) * (1 - n))) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((((1 - n) |^ 1) * (1 - n)) / ((1 - n) * (1 - n)))) is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(1 - n) |^ (1 + 1) is ext-real V14() real set
((1 - n) |^ (1 + 1)) / ((1 - n) * (1 - n)) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) |^ (1 + 1)) / ((1 - n) * (1 - n))) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - n) |^ (1 + 1)) / ((1 - n) * (1 - n)))) is ext-real V14() real set
1 |^ 2 is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * 1) * n is ext-real V14() real set
(1 |^ 2) - ((2 * 1) * n) is ext-real V14() real set
n |^ 2 is ext-real V14() real set
((1 |^ 2) - ((2 * 1) * n)) + (n |^ 2) is ext-real V14() real set
(((1 |^ 2) - ((2 * 1) * n)) + (n |^ 2)) / ((1 - n) * (1 - n)) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((((1 |^ 2) - ((2 * 1) * n)) + (n |^ 2)) / ((1 - n) * (1 - n))) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((((1 |^ 2) - ((2 * 1) * n)) + (n |^ 2)) / ((1 - n) * (1 - n)))) is ext-real V14() real set
(((1 |^ 2) - ((2 * 1) * n)) + (n |^ 2)) / ((1 - n) |^ 2) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((((1 |^ 2) - ((2 * 1) * n)) + (n |^ 2)) / ((1 - n) |^ 2)) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((((1 |^ 2) - ((2 * 1) * n)) + (n |^ 2)) / ((1 - n) |^ 2))) is ext-real V14() real set
2 * n is ext-real V14() real set
1 - (2 * n) is ext-real V14() real set
(1 - (2 * n)) + (n |^ 2) is ext-real V14() real set
((1 - (2 * n)) + (n |^ 2)) / ((1 - n) |^ 2) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - (2 * n)) + (n |^ 2)) / ((1 - n) |^ 2)) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + (((s * (n |^ (s + 1))) + (n |^ (s + 1))) * (((1 - (2 * n)) + (n |^ 2)) / ((1 - n) |^ 2))) is ext-real V14() real set
((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((1 - (2 * n)) + (n |^ 2)) is ext-real V14() real set
(((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((1 - (2 * n)) + (n |^ 2))) / ((1 - n) |^ 2) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) / ((1 - n) |^ 2)) + ((((s * (n |^ (s + 1))) + (n |^ (s + 1))) * ((1 - (2 * n)) + (n |^ 2))) / ((1 - n) |^ 2)) is ext-real V14() real set
(s * (n |^ (s + 1))) * 1 is ext-real V14() real set
(s * (n |^ (s + 1))) * 2 is ext-real V14() real set
((s * (n |^ (s + 1))) * 2) * n is ext-real V14() real set
((s * (n |^ (s + 1))) * 1) - (((s * (n |^ (s + 1))) * 2) * n) is ext-real V14() real set
(s * (n |^ (s + 1))) * (n |^ 2) is ext-real V14() real set
(((s * (n |^ (s + 1))) * 1) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2)) is ext-real V14() real set
(n |^ (s + 1)) * 1 is ext-real V14() real set
(n |^ (s + 1)) * 2 is ext-real V14() real set
((n |^ (s + 1)) * 2) * n is ext-real V14() real set
((n |^ (s + 1)) * 1) - (((n |^ (s + 1)) * 2) * n) is ext-real V14() real set
(n |^ (s + 1)) * (n |^ 2) is ext-real V14() real set
(((n |^ (s + 1)) * 1) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2)) is ext-real V14() real set
((((s * (n |^ (s + 1))) * 1) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2))) + ((((n |^ (s + 1)) * 1) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2))) is ext-real V14() real set
(((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) + (((((s * (n |^ (s + 1))) * 1) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2))) + ((((n |^ (s + 1)) * 1) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2)))) is ext-real V14() real set
((((n - (n * (n |^ s))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) + (((((s * (n |^ (s + 1))) * 1) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2))) + ((((n |^ (s + 1)) * 1) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2))))) / ((1 - n) |^ 2) is ext-real V14() real set
n - (n |^ (s + 1)) is ext-real V14() real set
(n - (n |^ (s + 1))) - (s * (n |^ (s + 1))) is ext-real V14() real set
((n - (n |^ (s + 1))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1))) is ext-real V14() real set
(s * (n |^ (s + 1))) - (((s * (n |^ (s + 1))) * 2) * n) is ext-real V14() real set
((s * (n |^ (s + 1))) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2)) is ext-real V14() real set
(n |^ (s + 1)) - (((n |^ (s + 1)) * 2) * n) is ext-real V14() real set
((n |^ (s + 1)) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2)) is ext-real V14() real set
(((s * (n |^ (s + 1))) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2))) + (((n |^ (s + 1)) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2))) is ext-real V14() real set
(((n - (n |^ (s + 1))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) + ((((s * (n |^ (s + 1))) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2))) + (((n |^ (s + 1)) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2)))) is ext-real V14() real set
((((n - (n |^ (s + 1))) - (s * (n |^ (s + 1)))) + ((n * s) * (n |^ (s + 1)))) + ((((s * (n |^ (s + 1))) - (((s * (n |^ (s + 1))) * 2) * n)) + ((s * (n |^ (s + 1))) * (n |^ 2))) + (((n |^ (s + 1)) - (((n |^ (s + 1)) * 2) * n)) + ((n |^ (s + 1)) * (n |^ 2))))) / ((1 - n) |^ 2) is ext-real V14() real set
(n |^ (s + 1)) * n is ext-real V14() real set
n - ((n |^ (s + 1)) * n) is ext-real V14() real set
(s + 1) * (n |^ (s + 1)) is ext-real V14() real set
n - (n |^ 2) is ext-real V14() real set
((s + 1) * (n |^ (s + 1))) * (n - (n |^ 2)) is ext-real V14() real set
(n - ((n |^ (s + 1)) * n)) - (((s + 1) * (n |^ (s + 1))) * (n - (n |^ 2))) is ext-real V14() real set
((n - ((n |^ (s + 1)) * n)) - (((s + 1) * (n |^ (s + 1))) * (n - (n |^ 2)))) / ((1 - n) |^ 2) is ext-real V14() real set
n * n is ext-real V14() real set
n - (n * n) is ext-real V14() real set
((s + 1) * (n |^ (s + 1))) * (n - (n * n)) is ext-real V14() real set
(n - ((n |^ (s + 1)) * n)) - (((s + 1) * (n |^ (s + 1))) * (n - (n * n))) is ext-real V14() real set
((n - ((n |^ (s + 1)) * n)) - (((s + 1) * (n |^ (s + 1))) * (n - (n * n)))) / ((1 - n) |^ 2) is ext-real V14() real set
(n - ((n |^ (s + 1)) * n)) / ((1 - n) |^ 2) is ext-real V14() real set
((s + 1) * (n |^ (s + 1))) * n is ext-real V14() real set
(((s + 1) * (n |^ (s + 1))) * n) * (1 - n) is ext-real V14() real set
((((s + 1) * (n |^ (s + 1))) * n) * (1 - n)) / ((1 - n) |^ 2) is ext-real V14() real set
((n - ((n |^ (s + 1)) * n)) / ((1 - n) |^ 2)) - (((((s + 1) * (n |^ (s + 1))) * n) * (1 - n)) / ((1 - n) |^ 2)) is ext-real V14() real set
((((s + 1) * (n |^ (s + 1))) * n) * (1 - n)) / ((1 - n) * (1 - n)) is ext-real V14() real set
((n - ((n |^ (s + 1)) * n)) / ((1 - n) |^ 2)) - (((((s + 1) * (n |^ (s + 1))) * n) * (1 - n)) / ((1 - n) * (1 - n))) is ext-real V14() real set
(((s + 1) * (n |^ (s + 1))) * n) / (1 - n) is ext-real V14() real set
((((s + 1) * (n |^ (s + 1))) * n) / (1 - n)) * (1 - n) is ext-real V14() real set
(((((s + 1) * (n |^ (s + 1))) * n) / (1 - n)) * (1 - n)) / (1 - n) is ext-real V14() real set
((n - ((n |^ (s + 1)) * n)) / ((1 - n) |^ 2)) - ((((((s + 1) * (n |^ (s + 1))) * n) / (1 - n)) * (1 - n)) / (1 - n)) is ext-real V14() real set
(s + 1) * ((n |^ (s + 1)) * n) is ext-real V14() real set
((s + 1) * ((n |^ (s + 1)) * n)) / (1 - n) is ext-real V14() real set
((n * (1 - (n |^ (s + 1)))) / ((1 - n) |^ 2)) - (((s + 1) * ((n |^ (s + 1)) * n)) / (1 - n)) is ext-real V14() real set
(s + 1) + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
n |^ ((s + 1) + 1) is ext-real V14() real set
(s + 1) * (n |^ ((s + 1) + 1)) is ext-real V14() real set
((s + 1) * (n |^ ((s + 1) + 1))) / (1 - n) is ext-real V14() real set
((n * (1 - (n |^ (s + 1)))) / ((1 - n) |^ 2)) - (((s + 1) * (n |^ ((s + 1) + 1))) / (1 - n)) is ext-real V14() real set
s is ext-real non negative ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
s + 2 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
2 -Root (s + 2) is ext-real V14() real Element of REAL
s + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
2 -Root (s + 1) is ext-real V14() real Element of REAL
(2 -Root (s + 2)) + (2 -Root (s + 1)) is ext-real V14() real set
1 / ((2 -Root (s + 2)) + (2 -Root (s + 1))) is ext-real V14() real set
(2 -Root (s + 2)) - (2 -Root (s + 1)) is ext-real V14() real set
(s + 1) + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(2 -Root (s + 1)) - (2 -Root (s + 1)) is ext-real V14() real set
(1 / ((2 -Root (s + 2)) + (2 -Root (s + 1)))) * 1 is ext-real V14() real set
1 * ((2 -Root (s + 2)) - (2 -Root (s + 1))) is ext-real V14() real set
((2 -Root (s + 2)) - (2 -Root (s + 1))) * ((2 -Root (s + 2)) + (2 -Root (s + 1))) is ext-real V14() real set
(1 * ((2 -Root (s + 2)) - (2 -Root (s + 1)))) / (((2 -Root (s + 2)) - (2 -Root (s + 1))) * ((2 -Root (s + 2)) + (2 -Root (s + 1)))) is ext-real V14() real set
(2 -Root (s + 2)) |^ 2 is ext-real V14() real Element of REAL
(2 -Root (s + 1)) |^ 2 is ext-real V14() real Element of REAL
((2 -Root (s + 2)) |^ 2) - ((2 -Root (s + 1)) |^ 2) is ext-real V14() real set
((2 -Root (s + 2)) - (2 -Root (s + 1))) / (((2 -Root (s + 2)) |^ 2) - ((2 -Root (s + 1)) |^ 2)) is ext-real V14() real set
(s + 2) - ((2 -Root (s + 1)) |^ 2) is ext-real V14() real set
((2 -Root (s + 2)) - (2 -Root (s + 1))) / ((s + 2) - ((2 -Root (s + 1)) |^ 2)) is ext-real V14() real set
(s + 2) - (s + 1) is ext-real V14() real set
((2 -Root (s + 2)) - (2 -Root (s + 1))) / ((s + 2) - (s + 1)) is ext-real V14() real set
s is ext-real V14() real set
s |^ 2 is ext-real V14() real set
2 * s is ext-real V14() real set
n is ext-real V14() real set
s + n is ext-real V14() real set
n |^ 2 is ext-real V14() real set
(s |^ 2) + (n |^ 2) is ext-real V14() real set
(2 * s) * n is ext-real V14() real set
2 * n is ext-real V14() real set
n is ext-real V14() real set
(s + n) + n is ext-real V14() real set
((s + n) + n) |^ 2 is ext-real V14() real set
n |^ 2 is ext-real V14() real set
((s |^ 2) + (n |^ 2)) + (n |^ 2) is ext-real V14() real set
(((s |^ 2) + (n |^ 2)) + (n |^ 2)) + ((2 * s) * n) is ext-real V14() real set
(2 * s) * n is ext-real V14() real set
((((s |^ 2) + (n |^ 2)) + (n |^ 2)) + ((2 * s) * n)) + ((2 * s) * n) is ext-real V14() real set
(2 * n) * n is ext-real V14() real set
(((((s |^ 2) + (n |^ 2)) + (n |^ 2)) + ((2 * s) * n)) + ((2 * s) * n)) + ((2 * n) * n) is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((s + n) + n) |^ (1 + 1) is ext-real V14() real set
((s + n) + n) |^ 1 is ext-real V14() real set
(((s + n) + n) |^ 1) * ((s + n) + n) is ext-real V14() real set
((s + n) + n) * ((s + n) + n) is ext-real V14() real set
s * s is ext-real V14() real set
s * n is ext-real V14() real set
(s * s) + (s * n) is ext-real V14() real set
s * n is ext-real V14() real set
((s * s) + (s * n)) + (s * n) is ext-real V14() real set
n * n is ext-real V14() real set
(s * n) + (n * n) is ext-real V14() real set
n * n is ext-real V14() real set
((s * n) + (n * n)) + (n * n) is ext-real V14() real set
(((s * s) + (s * n)) + (s * n)) + (((s * n) + (n * n)) + (n * n)) is ext-real V14() real set
n * n is ext-real V14() real set
(s * n) + (n * n) is ext-real V14() real set
n * n is ext-real V14() real set
((s * n) + (n * n)) + (n * n) is ext-real V14() real set
((((s * s) + (s * n)) + (s * n)) + (((s * n) + (n * n)) + (n * n))) + (((s * n) + (n * n)) + (n * n)) is ext-real V14() real set
(s * n) + (n |^ 2) is ext-real V14() real set
((s * n) + (n |^ 2)) + (n * n) is ext-real V14() real set
(((s * s) + (s * n)) + (s * n)) + (((s * n) + (n |^ 2)) + (n * n)) is ext-real V14() real set
((((s * s) + (s * n)) + (s * n)) + (((s * n) + (n |^ 2)) + (n * n))) + (((s * n) + (n * n)) + (n * n)) is ext-real V14() real set
(s |^ 2) + (s * n) is ext-real V14() real set
((s |^ 2) + (s * n)) + (s * n) is ext-real V14() real set
(((s |^ 2) + (s * n)) + (s * n)) + (((s * n) + (n |^ 2)) + (n * n)) is ext-real V14() real set
((((s |^ 2) + (s * n)) + (s * n)) + (((s * n) + (n |^ 2)) + (n * n))) + (((s * n) + (n * n)) + (n * n)) is ext-real V14() real set
((s * n) + (n * n)) + (n |^ 2) is ext-real V14() real set
((((s |^ 2) + (s * n)) + (s * n)) + (((s * n) + (n |^ 2)) + (n * n))) + (((s * n) + (n * n)) + (n |^ 2)) is ext-real V14() real set
(s |^ 2) + (n |^ 2) is ext-real V14() real set
((s |^ 2) + (n |^ 2)) + ((2 * s) * n) is ext-real V14() real set
(((s |^ 2) + (n |^ 2)) + ((2 * s) * n)) + ((2 * s) * n) is ext-real V14() real set
((((s |^ 2) + (n |^ 2)) + ((2 * s) * n)) + ((2 * s) * n)) + ((2 * n) * n) is ext-real V14() real set
(((((s |^ 2) + (n |^ 2)) + ((2 * s) * n)) + ((2 * s) * n)) + ((2 * n) * n)) + (n |^ 2) is ext-real V14() real set
s is ext-real V14() real set
s |^ 3 is ext-real V14() real set
s |^ 2 is ext-real V14() real set
3 * (s |^ 2) is ext-real V14() real set
n is ext-real V14() real set
s + n is ext-real V14() real set
(s + n) |^ 3 is ext-real V14() real set
(3 * (s |^ 2)) * n is ext-real V14() real set
(s |^ 3) + ((3 * (s |^ 2)) * n) is ext-real V14() real set
n |^ 2 is ext-real V14() real set
3 * (n |^ 2) is ext-real V14() real set
(3 * (n |^ 2)) * s is ext-real V14() real set
((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((3 * (n |^ 2)) * s) is ext-real V14() real set
n |^ 3 is ext-real V14() real set
(((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((3 * (n |^ 2)) * s)) + (n |^ 3) is ext-real V14() real set
2 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
(s + n) |^ (2 + 1) is ext-real V14() real set
(s + n) |^ 2 is ext-real V14() real set
((s + n) |^ 2) * (s + n) is ext-real V14() real set
2 * s is ext-real V14() real set
(2 * s) * n is ext-real V14() real set
(s |^ 2) + ((2 * s) * n) is ext-real V14() real set
((s |^ 2) + ((2 * s) * n)) + (n |^ 2) is ext-real V14() real set
(((s |^ 2) + ((2 * s) * n)) + (n |^ 2)) * (s + n) is ext-real V14() real set
(s |^ 2) * s is ext-real V14() real set
(s |^ 2) * n is ext-real V14() real set
((s |^ 2) * s) + ((s |^ 2) * n) is ext-real V14() real set
((2 * s) * n) * s is ext-real V14() real set
((2 * s) * n) * n is ext-real V14() real set
(((2 * s) * n) * s) + (((2 * s) * n) * n) is ext-real V14() real set
(((s |^ 2) * s) + ((s |^ 2) * n)) + ((((2 * s) * n) * s) + (((2 * s) * n) * n)) is ext-real V14() real set
(n |^ 2) * s is ext-real V14() real set
(n |^ 2) * n is ext-real V14() real set
((n |^ 2) * s) + ((n |^ 2) * n) is ext-real V14() real set
((((s |^ 2) * s) + ((s |^ 2) * n)) + ((((2 * s) * n) * s) + (((2 * s) * n) * n))) + (((n |^ 2) * s) + ((n |^ 2) * n)) is ext-real V14() real set
n |^ (2 + 1) is ext-real V14() real set
((n |^ 2) * s) + (n |^ (2 + 1)) is ext-real V14() real set
((((s |^ 2) * s) + ((s |^ 2) * n)) + ((((2 * s) * n) * s) + (((2 * s) * n) * n))) + (((n |^ 2) * s) + (n |^ (2 + 1))) is ext-real V14() real set
(s |^ 3) + ((s |^ 2) * n) is ext-real V14() real set
s * s is ext-real V14() real set
2 * (s * s) is ext-real V14() real set
(2 * (s * s)) * n is ext-real V14() real set
((2 * (s * s)) * n) + (((2 * s) * n) * n) is ext-real V14() real set
((s |^ 3) + ((s |^ 2) * n)) + (((2 * (s * s)) * n) + (((2 * s) * n) * n)) is ext-real V14() real set
((n |^ 2) * s) + (n |^ 3) is ext-real V14() real set
(((s |^ 3) + ((s |^ 2) * n)) + (((2 * (s * s)) * n) + (((2 * s) * n) * n))) + (((n |^ 2) * s) + (n |^ 3)) is ext-real V14() real set
s |^ 1 is ext-real V14() real set
(s |^ 1) * s is ext-real V14() real set
2 * ((s |^ 1) * s) is ext-real V14() real set
(2 * ((s |^ 1) * s)) * n is ext-real V14() real set
((2 * ((s |^ 1) * s)) * n) + (((2 * s) * n) * n) is ext-real V14() real set
((s |^ 3) + ((s |^ 2) * n)) + (((2 * ((s |^ 1) * s)) * n) + (((2 * s) * n) * n)) is ext-real V14() real set
(((s |^ 3) + ((s |^ 2) * n)) + (((2 * ((s |^ 1) * s)) * n) + (((2 * s) * n) * n))) + (((n |^ 2) * s) + (n |^ 3)) is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
s |^ (1 + 1) is ext-real V14() real set
2 * (s |^ (1 + 1)) is ext-real V14() real set
(2 * (s |^ (1 + 1))) * n is ext-real V14() real set
((2 * (s |^ (1 + 1))) * n) + (((2 * s) * n) * n) is ext-real V14() real set
((s |^ 3) + ((s |^ 2) * n)) + (((2 * (s |^ (1 + 1))) * n) + (((2 * s) * n) * n)) is ext-real V14() real set
(((s |^ 3) + ((s |^ 2) * n)) + (((2 * (s |^ (1 + 1))) * n) + (((2 * s) * n) * n))) + (((n |^ 2) * s) + (n |^ 3)) is ext-real V14() real set
n * n is ext-real V14() real set
2 * (n * n) is ext-real V14() real set
(2 * (n * n)) * s is ext-real V14() real set
((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((2 * (n * n)) * s) is ext-real V14() real set
(((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((2 * (n * n)) * s)) + (((n |^ 2) * s) + (n |^ 3)) is ext-real V14() real set
n |^ 1 is ext-real V14() real set
(n |^ 1) * n is ext-real V14() real set
2 * ((n |^ 1) * n) is ext-real V14() real set
(2 * ((n |^ 1) * n)) * s is ext-real V14() real set
((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((2 * ((n |^ 1) * n)) * s) is ext-real V14() real set
(((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((2 * ((n |^ 1) * n)) * s)) + (((n |^ 2) * s) + (n |^ 3)) is ext-real V14() real set
n |^ (1 + 1) is ext-real V14() real set
2 * (n |^ (1 + 1)) is ext-real V14() real set
(2 * (n |^ (1 + 1))) * s is ext-real V14() real set
((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((2 * (n |^ (1 + 1))) * s) is ext-real V14() real set
(((s |^ 3) + ((3 * (s |^ 2)) * n)) + ((2 * (n |^ (1 + 1))) * s)) + (((n |^ 2) * s) + (n |^ 3)) is ext-real V14() real set
s is ext-real V14() real set
s |^ 2 is ext-real V14() real set
2 * s is ext-real V14() real set
n is ext-real V14() real set
s - n is ext-real V14() real set
n |^ 2 is ext-real V14() real set
(s |^ 2) + (n |^ 2) is ext-real V14() real set
(2 * s) * n is ext-real V14() real set
2 * n is ext-real V14() real set
n is ext-real V14() real set
(s - n) + n is ext-real V14() real set
((s - n) + n) |^ 2 is ext-real V14() real set
n |^ 2 is ext-real V14() real set
((s |^ 2) + (n |^ 2)) + (n |^ 2) is ext-real V14() real set
(((s |^ 2) + (n |^ 2)) + (n |^ 2)) - ((2 * s) * n) is ext-real V14() real set
(2 * s) * n is ext-real V14() real set
((((s |^ 2) + (n |^ 2)) + (n |^ 2)) - ((2 * s) * n)) + ((2 * s) * n) is ext-real V14() real set
(2 * n) * n is ext-real V14() real set
(((((s |^ 2) + (n |^ 2)) + (n |^ 2)) - ((2 * s) * n)) + ((2 * s) * n)) - ((2 * n) * n) is ext-real V14() real set
1 + 1 is ext-real positive non negative V4() ordinal natural V14() real V33() V34() V57() V58() V59() V60() V61() V62() Element of NAT
((s - n) + n) |^ (1 + 1) is ext-real V14() real set
((s - n) + n) |^ 1 is ext-real V14() real set
(((s - n) + n) |^ 1) * ((s - n) + n) is ext-real V14() real set
((s - n) + n) * ((s - n) + n) is ext-real V14() real set
s * s is ext-real V14() real set
s * n is ext-real V14() real set
(s * s) - (s * n) is ext-real V14() real set
s * n is ext-real V14() real set
((s * s) - (s * n)) + (s * n) is ext-real V14() real set
n * n is ext-real V14() real set
(s * n) - (n * n) is ext-real V14() real set
n * n is ext-real V14() real set
((s * n) - (n * n)) + (n * n) is ext-real V14() real set
(((s * s) - (s * n)) + (s * n)) - (((s * n) - (n * n)) + (n * n)) is ext-real V14() real set
n * n is ext-real V14() real set
(s * n) - (n * n) is ext-real V14() real set
n * n is ext-real V14() real set
((s * n) - (n * n)) + (n * n) is ext-real V14() real set
((((s * s) - (s * n)) + (s * n)) - (((s * n) - (n * n)) + (n * n))) + (((s * n) - (n * n)) + (n * n)) is ext-real V14() real set
(s * n) - (n |^ 2) is ext-real V14() real set
((s * n) - (n |^ 2)) + (n * n) is ext-real V14() real set
(((s * s) - (s * n)) + (s * n)) - (((s * n) - (n |^ 2)) + (n * n)) is ext-real V14() real set
((((s * s) - (s * n)) + (s * n)) - (((s * n) - (n |^ 2)) + (n * n))) + (((s * n) - (n * n)) + (n * n)) is ext-real V14() real set
(s |^ 2) - (s * n) is ext-real V14() real set
((s |^ 2) - (s * n)) + (s * n) is ext-real V14() real set
(((s |^ 2) - (s * n)) + (s * n)) - (((s * n) - (n |^ 2)) + (n * n)) is ext-real V14() real set
((((s |^ 2) - (s * n)) + (s