:: MEMSTR_0 semantic presentation

REAL is non empty non trivial non with_non-empty_elements non empty-membered non finite V71() V72() V73() V77() set

NAT is non empty non trivial non with_non-empty_elements non empty-membered V27() V28() V29() V30() non finite cardinal limit_cardinal countable denumerable V71() V72() V73() V74() V75() V76() V77() Element of bool REAL

bool REAL is non empty non trivial non empty-membered non finite set

NAT is non empty non trivial non with_non-empty_elements non empty-membered V27() V28() V29() V30() non finite cardinal limit_cardinal countable denumerable V71() V72() V73() V74() V75() V76() V77() set

bool NAT is non empty non trivial non empty-membered non finite set

bool NAT is non empty non trivial non empty-membered non finite set

COMPLEX is non empty non trivial non empty-membered non finite V71() V77() set

RAT is non empty non trivial non empty-membered non finite V71() V72() V73() V74() V77() set

INT is non empty non trivial non empty-membered non finite V71() V72() V73() V74() V75() V77() set

{} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V27() V28() V29() V31() V32() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() V47() Cardinal-yielding countable V57() V58() V59() V61() V62() V63() V64() V65() V66() V67() V68() V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

the empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V27() V28() V29() V31() V32() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() V47() Cardinal-yielding countable V57() V58() V59() V61() V62() V63() V64() V65() V66() V67() V68() V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V27() V28() V29() V31() V32() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() V47() Cardinal-yielding countable V57() V58() V59() V61() V62() V63() V64() V65() V66() V67() V68() V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

2 is non empty ext-real positive non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

1 is non empty ext-real positive non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

3 is non empty ext-real positive non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

dom {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V27() V28() V29() V31() V32() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() V47() Cardinal-yielding countable V57() V58() V59() V61() V62() V63() V64() V65() V66() V67() V68() V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

rng {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V27() V28() V29() V31() V32() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() V47() Cardinal-yielding countable V57() V58() V59() V61() V62() V63() V64() V65() V66() V67() V68() V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial set

0 is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V27() V28() V29() V31() V32() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() V47() Cardinal-yielding countable V57() V58() V59() V60() V61() V62() V63() V64() V65() V66() V67() V68() V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() initial Element of NAT

N is non with_non-empty_elements set

{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() Element of bool NAT

0 .--> 0 is non empty trivial Relation-like NAT -defined {0} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant Function-yielding V35() finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() set

{0} --> 0 is non empty Relation-like {0} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V21({0},{0}) Function-yielding V35() finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{0},{0}:]

[:{0},{0}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{0},{0}:] is non empty finite V40() countable set

N --> NAT is Relation-like non-empty N -defined bool REAL -valued Function-like constant total V21(N, bool REAL) Cardinal-yielding Element of bool [:N,(bool REAL):]

[:N,(bool REAL):] is Relation-like set

bool [:N,(bool REAL):] is non empty set

{NAT} is non empty trivial with_non-empty_elements non empty-membered finite 1 -element countable set

[:N,{NAT}:] is Relation-like set

dom (0 .--> 0) is non empty trivial finite 1 -element countable V71() V72() V73() V74() V75() V76() set

rng (0 .--> 0) is non empty trivial finite 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{0},N:] is Relation-like set

bool [:{0},N:] is non empty set

s2 is Relation-like Function-like ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V93() Element of {0}

f is Relation-like {0} -defined N -valued Function-like V21({0},N) finite countable V93() Element of bool [:{0},N:]

(N,{0},s2,f,(N --> NAT)) is (N) (N)

the carrier of (N,{0},s2,f,(N --> NAT)) is set

the ZeroF of (N,{0},s2,f,(N --> NAT)) is Element of the carrier of (N,{0},s2,f,(N --> NAT))

the of (N,{0},s2,f,(N --> NAT)) is Relation-like the carrier of (N,{0},s2,f,(N --> NAT)) -defined N -valued Function-like V21( the carrier of (N,{0},s2,f,(N --> NAT)),N) Element of bool [: the carrier of (N,{0},s2,f,(N --> NAT)),N:]

[: the carrier of (N,{0},s2,f,(N --> NAT)),N:] is Relation-like set

bool [: the carrier of (N,{0},s2,f,(N --> NAT)),N:] is non empty set

the of (N,{0},s2,f,(N --> NAT)) is Relation-like N -defined Function-like total set

S is (N) (N)

the carrier of S is set

the ZeroF of S is Element of the carrier of S

the of S is Relation-like the carrier of S -defined N -valued Function-like V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is Relation-like N -defined Function-like total set

f is (N) (N)

the carrier of f is set

the ZeroF of f is Element of the carrier of f

the of f is Relation-like the carrier of f -defined N -valued Function-like V21( the carrier of f,N) Element of bool [: the carrier of f,N:]

[: the carrier of f,N:] is Relation-like set

bool [: the carrier of f,N:] is non empty set

the of f is Relation-like N -defined Function-like total set

N is non with_non-empty_elements set

(N) is (N) (N)

the carrier of (N) is set

N is non with_non-empty_elements set

(N) is non empty trivial finite 1 -element (N) (N)

N is non with_non-empty_elements set

N is set

N is non empty non with_non-empty_elements set

S is (N)

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

the carrier of S is set

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set

(N) is non empty trivial finite 1 -element (N) (N)

S is set

(N,(N)) is non empty Relation-like the carrier of (N) -defined Function-like total V93() set

the carrier of (N) is non empty trivial finite 1 -element countable set

the of (N) is non empty Relation-like the carrier of (N) -defined N -valued Function-like total V21( the carrier of (N),N) finite countable V93() Element of bool [: the carrier of (N),N:]

[: the carrier of (N),N:] is non empty Relation-like set

bool [: the carrier of (N),N:] is non empty set

the of (N) is non empty Relation-like N -defined Function-like total set

the of (N) * the of (N) is non empty Relation-like the carrier of (N) -defined Function-like total finite countable V93() set

dom (N,(N)) is non empty set

(N,(N)) . S is set

the of (N) . S is set

dom the of (N) is non empty set

N --> NAT is non empty Relation-like non-empty non empty-yielding N -defined bool REAL -valued Function-like constant total V21(N, bool REAL) Cardinal-yielding Element of bool [:N,(bool REAL):]

[:N,(bool REAL):] is non empty non trivial non empty-membered Relation-like non finite set

bool [:N,(bool REAL):] is non empty non trivial non empty-membered non finite set

[:N,{NAT}:] is non empty Relation-like set

the of (N) . ( the of (N) . S) is set

N is non empty non with_non-empty_elements set

(N) is non empty trivial finite 1 -element (N) (N) (N)

N is non empty non with_non-empty_elements set

S is (N) (N)

(N,S) is Relation-like the carrier of S -defined Function-like total set

the carrier of S is set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set

S is non empty (N)

the carrier of S is non empty set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

f is Element of the carrier of S

the of S . f is Element of N

N is non empty non with_non-empty_elements set

S is non empty (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is Element of the carrier of S

(N,S) . f is set

N is non empty non with_non-empty_elements set

0 .--> NAT is non empty trivial Relation-like NAT -defined {0} -defined bool REAL -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V93() set

{0} --> NAT is non empty Relation-like non-empty non empty-yielding {0} -defined bool REAL -valued {NAT} -valued Function-like constant total V21({0},{NAT}) finite Cardinal-yielding countable V93() Element of bool [:{0},{NAT}:]

[:{0},{NAT}:] is non empty Relation-like finite countable set

bool [:{0},{NAT}:] is non empty finite V40() countable set

N is non empty non with_non-empty_elements set

(N) is non empty trivial finite 1 -element (N) (N) (N)

(N,(N)) is non empty Relation-like non-empty non empty-yielding the carrier of (N) -defined Function-like total V93() set

the carrier of (N) is non empty trivial finite 1 -element countable set

the of (N) is non empty Relation-like the carrier of (N) -defined N -valued Function-like total V21( the carrier of (N),N) finite countable V93() Element of bool [: the carrier of (N),N:]

[: the carrier of (N),N:] is non empty Relation-like set

bool [: the carrier of (N),N:] is non empty set

the of (N) is non empty Relation-like N -defined Function-like total set

the of (N) * the of (N) is non empty Relation-like the carrier of (N) -defined Function-like total finite countable V93() set

N --> NAT is non empty Relation-like non-empty non empty-yielding N -defined bool REAL -valued Function-like constant total V21(N, bool REAL) Cardinal-yielding Element of bool [:N,(bool REAL):]

[:N,(bool REAL):] is non empty non trivial non empty-membered Relation-like non finite set

bool [:N,(bool REAL):] is non empty non trivial non empty-membered non finite set

[:N,{NAT}:] is non empty Relation-like set

(0 .--> 0) * (N --> NAT) is Relation-like non-empty NAT -defined bool REAL -valued Function-like finite countable V93() set

dom (N --> NAT) is non empty set

rng (0 .--> 0) is non empty trivial finite 1 -element countable V71() V72() V73() V74() V75() V76() set

dom (N,(N)) is non empty set

dom (0 .--> 0) is non empty trivial finite 1 -element countable V71() V72() V73() V74() V75() V76() set

dom (0 .--> NAT) is non empty trivial finite 1 -element countable V71() V72() V73() V74() V75() V76() set

S1 is set

(N,(N)) . S1 is set

(0 .--> NAT) . S1 is set

(0 .--> 0) . S1 is Relation-like Function-like ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V93() set

(N --> NAT) . ((0 .--> 0) . S1) is set

(N --> NAT) . 0 is set

N is non empty non with_non-empty_elements set

(N) is non empty trivial finite 1 -element (N) (N) (N)

0. (N) is V110((N)) Element of the carrier of (N)

the carrier of (N) is non empty trivial finite 1 -element countable set

the ZeroF of (N) is Element of the carrier of (N)

(N,(N),(0. (N))) is set

(N,(N)) is non empty Relation-like non-empty non empty-yielding the carrier of (N) -defined Function-like total V93() set

the of (N) is non empty Relation-like the carrier of (N) -defined N -valued Function-like total V21( the carrier of (N),N) finite countable V93() Element of bool [: the carrier of (N),N:]

[: the carrier of (N),N:] is non empty Relation-like set

bool [: the carrier of (N),N:] is non empty set

the of (N) is non empty Relation-like N -defined Function-like total set

the of (N) * the of (N) is non empty Relation-like the carrier of (N) -defined Function-like total finite countable V93() set

(N,(N)) . (0. (N)) is non empty set

(0 .--> NAT) . 0 is set

N is non empty non with_non-empty_elements set

(N) is non empty trivial finite 1 -element (N) (N) (N) (N)

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f . (0. S) is set

dom f is set

s2 is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

product (N,S) is non empty functional with_common_domain product-like set

dom (N,S) is non empty set

pi ((product (N,S)),(0. S)) is set

(N,S,(0. S)) is set

(N,S) . (0. S) is non empty set

S1 is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total Element of product (N,S)

S1 . (0. S) is set

dom f is set

dom f is set

N is non empty non with_non-empty_elements set

S is non empty trivial finite 1 -element (N) (N) (N)

the carrier of S is non empty trivial finite 1 -element countable set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total V93() set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) finite countable V93() Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total finite countable V93() set

f is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total V93() set

(N,S,f) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f . (0. S) is set

s2 is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total V93() set

(N,S,s2) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

s2 . (0. S) is set

dom f is non empty set

dom s2 is non empty set

S1 is set

f . S1 is set

s2 . S1 is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N)

the carrier of S is non empty set

f is Element of the carrier of S

(N,S,f) is set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

(N,S) . f is non empty set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

f is Element of the carrier of S

(N,S,f) is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

(N,S) . f is non empty set

s2 is Element of (N,S,f)

f .--> s2 is non empty trivial Relation-like the carrier of S -defined {f} -defined (N,S,f) -valued Function-like one-to-one constant finite 1 -element countable V93() set

{f} is non empty trivial finite 1 -element countable set

{f} --> s2 is non empty Relation-like {f} -defined (N,S,f) -valued {s2} -valued Function-like constant total V21({f},{s2}) finite countable V93() Element of bool [:{f},{s2}:]

{s2} is non empty trivial finite 1 -element countable set

[:{f},{s2}:] is non empty Relation-like finite countable set

bool [:{f},{s2}:] is non empty finite V40() countable set

dom (f .--> s2) is non empty trivial finite 1 -element countable set

{f} is non empty trivial finite 1 -element countable Element of bool the carrier of S

bool the carrier of S is non empty set

S2 is set

(f .--> s2) . S2 is set

(N,S) . S2 is set

S1 is Element of the carrier of S

(N,S,S1) is non empty set

(N,S) . S1 is non empty set

S2 is Element of (N,S,S1)

(f,S1) --> (s2,S2) is non empty Relation-like the carrier of S -defined Function-like finite countable V93() set

S1 .--> S2 is non empty trivial Relation-like the carrier of S -defined {S1} -defined the carrier of S -defined (N,S,S1) -valued (N,S,S1) -valued Function-like one-to-one constant (N,S) -compatible finite 1 -element countable V93() set

{S1} is non empty trivial finite 1 -element countable set

{S1} --> S2 is non empty Relation-like {S1} -defined (N,S,S1) -valued {S2} -valued Function-like constant total V21({S1},{S2}) finite countable V93() Element of bool [:{S1},{S2}:]

{S2} is non empty trivial finite 1 -element countable set

[:{S1},{S2}:] is non empty Relation-like finite countable set

bool [:{S1},{S2}:] is non empty finite V40() countable set

(f .--> s2) +* (S1 .--> S2) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible finite countable V93() set

N is non empty non with_non-empty_elements set

S is non empty (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

dom f is non empty set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

s2 is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

S1 is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

S1 | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

s2 | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

dom f is set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non proper Element of bool the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

dom (N,S,f) is set

the carrier of S \ {(0. S)} is Element of bool the carrier of S

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non proper Element of bool the carrier of S

([#] S) \ {(0. S)} is Element of bool the carrier of S

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

dom (N,S,f) is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

s2 is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,s2) is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non empty non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

s2 | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

{(0. S)} is non empty trivial finite 1 -element countable Element of bool the carrier of S

the carrier of S \ {(0. S)} is Element of bool the carrier of S

s2 | ( the carrier of S \ {(0. S)}) is Relation-like the carrier of S \ {(0. S)} -defined the carrier of S -defined Function-like (N,S) -compatible set

( the carrier of S \ {(0. S)}) \/ {(0. S)} is non empty Element of bool the carrier of S

the carrier of S \/ {(0. S)} is non empty set

dom f is set

f | ( the carrier of S \ {(0. S)}) is Relation-like the carrier of S \ {(0. S)} -defined the carrier of S -defined Function-like (N,S) -compatible set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

dom (N,S,f) is set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

dom f is set

N is non empty non with_non-empty_elements set

S is (N)

the carrier of S is set

(N,S) is Relation-like the carrier of S -defined Function-like total set

the of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

dom f is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non empty non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

dom f is non empty set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non empty non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

dom (N,S,f) is set

dom f is non empty set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

dom f is set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non empty non proper Element of bool the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,f) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f . (0. S) is set

s2 is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

f +* s2 is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,(f +* s2)) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

(f +* s2) . (0. S) is set

dom s2 is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non empty non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable Element of bool the carrier of S

bool the carrier of S is non empty set

NonZero S is Element of bool the carrier of S

[#] S is non empty non proper Element of bool the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

{(0. S)} \/ (NonZero S) is non empty Element of bool the carrier of S

f is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

dom f is non empty set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

dom f is set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non empty non proper Element of bool the carrier of S

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable set

([#] S) \ {(0. S)} is Element of bool the carrier of S

(dom f) /\ (NonZero S) is Element of bool the carrier of S

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

dom (N,S,f) is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

s2 is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

s2 +* ((0. S),f) is non empty Relation-like the carrier of S -defined Function-like total set

S1 is set

dom (s2 +* ((0. S),f)) is non empty set

(s2 +* ((0. S),f)) . S1 is set

(N,S) . S1 is set

dom s2 is non empty set

(N,S,(0. S)) is non empty set

(N,S) . (0. S) is non empty set

s2 . S1 is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

0. S is V110(S) Element of the carrier of S

the carrier of S is non empty set

the ZeroF of S is Element of the carrier of S

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

(0. S) .--> f is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined RAT -valued INT -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{(0. S)} is non empty trivial finite 1 -element countable set

{(0. S)} --> f is non empty Relation-like {(0. S)} -defined RAT -valued INT -valued {f} -valued Function-like constant total V21({(0. S)},{f}) finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{(0. S)},{f}:]

{f} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{(0. S)},{f}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{(0. S)},{f}:] is non empty finite V40() countable set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

(N,S,(0. S)) is non empty set

(N,S) . (0. S) is non empty set

s2 is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

S1 is Element of (N,S,(0. S))

(0. S) .--> S1 is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined the carrier of S -defined (N,S,(0. S)) -valued (N,S,(0. S)) -valued Function-like one-to-one constant (N,S) -compatible finite 1 -element countable V93() set

{(0. S)} --> S1 is non empty Relation-like {(0. S)} -defined (N,S,(0. S)) -valued {S1} -valued Function-like constant total V21({(0. S)},{S1}) finite countable V93() Element of bool [:{(0. S)},{S1}:]

{S1} is non empty trivial finite 1 -element countable set

[:{(0. S)},{S1}:] is non empty Relation-like finite countable set

bool [:{(0. S)},{S1}:] is non empty finite V40() countable set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

(0. S) .--> f is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined RAT -valued INT -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{(0. S)} is non empty trivial finite 1 -element countable set

{(0. S)} --> f is non empty Relation-like {(0. S)} -defined RAT -valued INT -valued {f} -valued Function-like constant total V21({(0. S)},{f}) finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{(0. S)},{f}:]

{f} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{(0. S)},{f}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{(0. S)},{f}:] is non empty finite V40() countable set

dom (N,S,f) is set

{(0. S)} is non empty trivial finite 1 -element countable Element of bool the carrier of S

bool the carrier of S is non empty set

(N,S,(N,S,f)) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

(N,S,f) . (0. S) is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

0. S is V110(S) Element of the carrier of S

the carrier of S is non empty set

the ZeroF of S is Element of the carrier of S

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

(N,S,f) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S,f) set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

(0. S) .--> f is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined RAT -valued INT -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{(0. S)} is non empty trivial finite 1 -element countable set

{(0. S)} --> f is non empty Relation-like {(0. S)} -defined RAT -valued INT -valued {f} -valued Function-like constant total V21({(0. S)},{f}) finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{(0. S)},{f}:]

{f} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{(0. S)},{f}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{(0. S)},{f}:] is non empty finite V40() countable set

dom (N,S,f) is non empty set

{(0. S)} is non empty trivial finite 1 -element countable Element of bool the carrier of S

bool the carrier of S is non empty set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

s2 is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

(N,S,s2) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S,s2) set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

(0. S) .--> s2 is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined RAT -valued INT -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{(0. S)} is non empty trivial finite 1 -element countable set

{(0. S)} --> s2 is non empty Relation-like {(0. S)} -defined RAT -valued INT -valued {s2} -valued Function-like constant total V21({(0. S)},{s2}) finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{(0. S)},{s2}:]

{s2} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{(0. S)},{s2}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{(0. S)},{s2}:] is non empty finite V40() countable set

f +* (N,S,s2) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible set

(N,S,(f +* (N,S,s2))) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

(f +* (N,S,s2)) . (0. S) is set

dom (N,S,s2) is non empty set

(N,S,s2) . (0. S) is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

the non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

(N,S,f) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S,f) set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

(0. S) .--> f is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined RAT -valued INT -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{(0. S)} is non empty trivial finite 1 -element countable set

{(0. S)} --> f is non empty Relation-like {(0. S)} -defined RAT -valued INT -valued {f} -valued Function-like constant total V21({(0. S)},{f}) finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{(0. S)},{f}:]

{f} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{(0. S)},{f}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{(0. S)},{f}:] is non empty finite V40() countable set

the non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set +* (N,S,f) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

s2 is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

dom s2 is non empty set

(N,S,s2) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

s2 . (0. S) is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

s2 is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

S1 is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S,f) set

s2 +* S1 is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

dom S1 is set

dom (s2 +* S1) is set

(N,S,(s2 +* S1)) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

(s2 +* S1) . (0. S) is set

(N,S,S1) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

S1 . (0. S) is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

s2 is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

(N,S,s2) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

s2 . (0. S) is set

dom s2 is non empty set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

f is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() set

s2 is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S,f) set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

dom s2 is set

(N,S,s2) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

s2 . (0. S) is set

S1 is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

dom S1 is set

(N,S,S1) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

S1 . (0. S) is set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

{(0. S)} is non empty trivial finite 1 -element countable Element of bool the carrier of S

bool the carrier of S is non empty set

f is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible total set

(N,S,f) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

f . (0. S) is set

(N,S,(N,S,f)) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S,(N,S,f)) set

(0. S) .--> (N,S,f) is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{(0. S)} is non empty trivial finite 1 -element countable set

{(0. S)} --> (N,S,f) is non empty Relation-like {(0. S)} -defined NAT -valued RAT -valued INT -valued {(N,S,f)} -valued Function-like constant total V21({(0. S)},{(N,S,f)}) finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{(0. S)},{(N,S,f)}:]

{(N,S,f)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{(0. S)},{(N,S,f)}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{(0. S)},{(N,S,f)}:] is non empty finite V40() countable set

f | {(0. S)} is Relation-like {(0. S)} -defined the carrier of S -defined Function-like (N,S) -compatible finite countable V93() set

dom f is non empty set

[(0. S),(f . (0. S))] is non empty set

{(0. S),(f . (0. S))} is non empty finite countable set

{{(0. S),(f . (0. S))},{(0. S)}} is non empty with_non-empty_elements non empty-membered finite V40() countable set

{[(0. S),(f . (0. S))]} is non empty trivial with_non-empty_elements non empty-membered Relation-like Function-like constant finite 1 -element countable V93() set

N is non empty non with_non-empty_elements set

S is non empty (N) (N) (N)

the carrier of S is non empty set

(N,S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

the of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]

[: the carrier of S,N:] is non empty Relation-like set

bool [: the carrier of S,N:] is non empty set

the of S is non empty Relation-like N -defined Function-like total set

the of S * the of S is non empty Relation-like the carrier of S -defined Function-like total set

0. S is V110(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

f is Relation-like the carrier of S -defined Function-like (N,S) -compatible set

dom f is set

(N,S,f) is ext-real non negative V27() V28() V29() V33() finite cardinal countable V57() V58() V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

f . (0. S) is set

(N,S,(N,S,f)) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S,(N,S,f)) set

(0. S) .--> (N,S,f) is non empty trivial Relation-like the carrier of S -defined {(0. S)} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V61() V62() V63() V64() V65() V66() V67() V68() V93() set

{(0. S)} is non empty trivial finite 1 -element countable set

{(0. S)} --> (N,S,f) is non empty Relation-like {(0. S)} -defined NAT -valued RAT -valued INT -valued {(N,S,f)} -valued Function-like constant total V21({(0. S)},{(N,S,f)}) finite Cardinal-yielding countable V61() V62() V63() V64() V93() Element of bool [:{(0. S)},{(N,S,f)}:]

{(N,S,f)} is non empty trivial finite V40() 1 -element countable V71() V72() V73() V74() V75() V76() set

[:{(0. S)},{(N,S,f)}:] is non empty Relation-like RAT -valued INT -valued finite countable V61() V62() V63() V64() set

bool [:{(0. S)},{(N,S,f)}:] is non empty finite V40() countable set

(N,S,f) is Relation-like the carrier of S -defined Function-like (N,S) -compatible (N,S) set

NonZero S is Element of bool the carrier of S

bool the carrier of S is non empty set

[#] S is non empty non proper Element of bool the carrier of S

([#] S) \ {(0. S)} is Element of bool the carrier of S

f | (NonZero S) is Relation-like NonZero S -defined the carrier of S -defined Function-like (N,S) -compatible set

(N,S,(N,S,f)) +* (N,S,f) is non empty Relation-like the carrier of S -defined Function-like (N,S) -compatible set

{(0. S)} is non empty trivial finite 1 -element countable Element of bool the carrier of S

bool (dom f) is non empty set

the carrier of S \ {(0. S)} is Element of bool the carrier of S

{(0. S)} \/ ( the carrier of S \ {(0. S)}) is non empty Element of bool the carrier of S

the carrier of S \/ {(0. S)} is non empty set

s2 is set

dom (N,S,(N,S,f)) is non empty set

dom (N,S,f) is set

(dom (N,S,(N,S,f))) \/ (dom (N,S,f)) is non empty set

((N,S,(N,S,f)) +* (N,S,f)) . s2 is set

(N,S,(N,S,f)) . s2 is set

f . s2 is set

(dom f) /\ ( the carrier of S \ {(0. S)}) is Element of bool the carrier of S

f | ( the carrier of S \ {(0. S)}) is Relation-like the carrier of S \ {(0. S)} -defined the carrier of S -defined Function-like (N,S) -compatible set

dom (f | ( the carrier of S \ {(0. S)})) is set

((N,S,(N,S,f)) +* (N,S,f)) . s2 is set

(N,S,f) . s2 is set

f . s2 is set

dom ((N,S,(N,S,f)) +* (N,S,f)) is non empty set

dom (N,S,(N,S,f)) is non empty set

dom (N,S,f) is set

(dom (N,S,(N,S,f))) \/ (dom (N,S,f)) is non empty set

{(0. S)} \/ (