REAL is non empty non trivial non finite set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() set
RAT is non empty non trivial non finite set
the empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() set is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() set
1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
{{},1} is non empty finite V60() set
COMPLEX is non empty non trivial non finite set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial Relation-like non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial Relation-like non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial Relation-like non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial Relation-like non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
[:COMPLEX,REAL:] is non empty non trivial Relation-like non finite set
bool [:COMPLEX,REAL:] is non empty non trivial non finite set
2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
3 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() Element of NAT
union {} is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
dom {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() set
rng {} is empty trivial V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() V39() V42() V43() V44() V45() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V201() V205() set
card {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() set
{{}} is non empty trivial functional finite V60() 1 -element set
addint is non empty Relation-like [:INT,INT:] -defined INT -valued Function-like V25([:INT,INT:]) quasi_total V32() V33() V34() V128( INT ) commutative associative Element of bool [:[:INT,INT:],INT:]
addnat is non empty Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V25([:NAT,NAT:]) quasi_total V32() V33() V34() V35() V52() V128( NAT ) commutative associative Element of bool [:[:NAT,NAT:],NAT:]
the_unity_wrt addint is V11() ext-real V53() integer Element of INT
0 ! is V11() ext-real V53() Element of REAL
Funcs ({},{}) is non empty functional finite set
id {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional V25( {} ) V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() set
{(id {})} is non empty trivial functional finite V60() 1 -element set
X is finite set
card X is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S1 is finite set
card S1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S1 \ X is finite Element of bool S1
bool S1 is non empty finite V60() set
card (S1 \ X) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card S1) - (card X) is V11() ext-real V53() integer Element of INT
X is finite set
S1 is finite set
Funcs (X,S1) is functional finite set
card (Funcs (X,S1)) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S2 is set
{S2} is non empty trivial finite 1 -element set
X \/ {S2} is non empty finite set
x is set
{x} is non empty trivial finite 1 -element set
S1 \/ {x} is non empty finite set
[:(X \/ {S2}),(S1 \/ {x}):] is non empty Relation-like finite set
bool [:(X \/ {S2}),(S1 \/ {x}):] is non empty finite V60() set
{ b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( rng (b1 | X) c= S1 & b1 . S2 = x ) } is set
card { b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( rng (b1 | X) c= S1 & b1 . S2 = x ) } is V4() V5() V6() cardinal set
{ b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( S1[b1,X \/ {S2},S1 \/ {x}] & rng (b1 | X) c= S1 & b1 . S2 = x ) } is set
y is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
y . S2 is set
[:X,S1:] is Relation-like finite set
bool [:X,S1:] is non empty finite V60() set
{ b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : S1[b1,X,S1] } is set
F1 is set
F1 is set
F1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
F1 | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
rng (F1 | X) is finite Element of bool (S1 \/ {x})
bool (S1 \/ {x}) is non empty finite V60() set
F1 . S2 is set
card { b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : S1[b1,X,S1] } is V4() V5() V6() cardinal set
card { b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( S1[b1,X \/ {S2},S1 \/ {x}] & rng (b1 | X) c= S1 & b1 . S2 = x ) } is V4() V5() V6() cardinal set
F1 is set
F1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
F1 | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
rng (F1 | X) is finite Element of bool (S1 \/ {x})
bool (S1 \/ {x}) is non empty finite V60() set
F1 . S2 is set
F1 is set
F1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:]
X is finite set
S1 is finite set
Funcs (X,S1) is functional finite set
card (Funcs (X,S1)) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S2 is set
{S2} is non empty trivial finite 1 -element set
X \/ {S2} is non empty finite set
[:(X \/ {S2}),S1:] is Relation-like finite set
bool [:(X \/ {S2}),S1:] is non empty finite V60() set
x is set
{ b1 where b1 is Relation-like X \/ {S2} -defined S1 -valued Function-like quasi_total finite Element of bool [:(X \/ {S2}),S1:] : b1 . S2 = x } is set
card { b1 where b1 is Relation-like X \/ {S2} -defined S1 -valued Function-like quasi_total finite Element of bool [:(X \/ {S2}),S1:] : b1 . S2 = x } is V4() V5() V6() cardinal set
{x} is non empty trivial finite 1 -element set
S1 \/ {x} is non empty finite set
[:(X \/ {S2}),(S1 \/ {x}):] is non empty Relation-like finite set
bool [:(X \/ {S2}),(S1 \/ {x}):] is non empty finite V60() set
{ b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( rng (b1 | X) c= S1 & b1 . S2 = x ) } is set
c is set
F1 is Relation-like X \/ {S2} -defined S1 -valued Function-like quasi_total finite Element of bool [:(X \/ {S2}),S1:]
F1 . S2 is set
F1 | X is Relation-like X -defined X \/ {S2} -defined S1 -valued Function-like finite Element of bool [:(X \/ {S2}),S1:]
rng (F1 | X) is finite Element of bool S1
bool S1 is non empty finite V60() set
c is set
F1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
F1 | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
rng (F1 | X) is finite Element of bool (S1 \/ {x})
bool (S1 \/ {x}) is non empty finite V60() set
F1 . S2 is set
X is finite set
card X is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S1 is finite set
Funcs (S1,X) is functional finite set
card (Funcs (S1,X)) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
card S1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card X) |^ (card S1) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S2 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
S2 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
x is finite set
card x is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
h is finite set
Funcs (x,h) is functional finite set
card (Funcs (x,h)) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
card h is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card h) |^ (card x) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
y is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card h) |^ y is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
F1 is Relation-like Function-like set
dom F1 is set
rng F1 is set
[:(card h),h:] is Relation-like finite set
bool [:(card h),h:] is non empty finite V60() set
XF is set
F1 is Relation-like card h -defined h -valued Function-like quasi_total finite Element of bool [:(card h),h:]
[:x,h:] is Relation-like finite set
bool [:x,h:] is non empty finite V60() set
{ b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : S2[b1] } is set
card { b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : S2[b1] } is V4() V5() V6() cardinal set
n is V8() Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() V52() finite V205() set
dom n is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of bool NAT
Sum n is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of COMPLEX
c is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
{XF} is non empty trivial finite 1 -element set
x \ {XF} is finite Element of bool x
bool x is non empty finite V60() set
u is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
n . u is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
F1 . u is set
rng F1 is finite Element of bool h
bool h is non empty finite V60() set
{ b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : ( S2[b1] & b1 . XF = F1 . u ) } is set
(x \ {XF}) \/ {XF} is non empty finite set
[:((x \ {XF}) \/ {XF}),h:] is Relation-like finite set
bool [:((x \ {XF}) \/ {XF}),h:] is non empty finite V60() set
{ b1 where b1 is Relation-like (x \ {XF}) \/ {XF} -defined h -valued Function-like quasi_total finite Element of bool [:((x \ {XF}) \/ {XF}),h:] : b1 . XF = F1 . u } is set
Fyy is set
y is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:]
y . XF is set
Fyy is set
y is Relation-like (x \ {XF}) \/ {XF} -defined h -valued Function-like quasi_total finite Element of bool [:((x \ {XF}) \/ {XF}),h:]
y . XF is set
card (x \ {XF}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
Funcs ((x \ {XF}),h) is functional finite set
card (Funcs ((x \ {XF}),h)) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
card { b1 where b1 is Relation-like (x \ {XF}) \/ {XF} -defined h -valued Function-like quasi_total finite Element of bool [:((x \ {XF}) \/ {XF}),h:] : b1 . XF = F1 . u } is V4() V5() V6() cardinal set
n1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
n . n1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
len n is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
dom n is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
(card h) |^ S2 is V11() ext-real V53() integer set
(len n) * ((card h) |^ S2) is V11() ext-real V53() integer Element of INT
u is set
u is set
n is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:]
u is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
n . u is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card h) * ((card h) |^ S2) is V11() ext-real V53() integer Element of INT
S2 is finite set
card S2 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
x is finite set
Funcs (S2,x) is functional finite set
card (Funcs (S2,x)) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
card x is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card x) |^ (card S2) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
X is finite set
S1 is finite set
[:X,S1:] is Relation-like finite set
bool [:X,S1:] is non empty finite V60() set
{ b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : b1 is one-to-one } is set
card { b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : b1 is one-to-one } is V4() V5() V6() cardinal set
S2 is set
{S2} is non empty trivial finite 1 -element set
X \/ {S2} is non empty finite set
x is set
{x} is non empty trivial finite 1 -element set
S1 \/ {x} is non empty finite set
[:(X \/ {S2}),(S1 \/ {x}):] is non empty Relation-like finite set
bool [:(X \/ {S2}),(S1 \/ {x}):] is non empty finite V60() set
{ b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( b1 is one-to-one & b1 . S2 = x ) } is set
card { b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( b1 is one-to-one & b1 . S2 = x ) } is V4() V5() V6() cardinal set
h is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
h . S2 is set
h | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite set
rng (h | X) is finite set
h | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
(h | X) | X is Relation-like X -defined X -defined S1 \/ {x} -valued Function-like finite set
rng ((h | X) | X) is finite set
(X \/ {S2}) /\ X is finite set
dom h is non empty finite Element of bool (X \/ {S2})
bool (X \/ {S2}) is non empty finite V60() set
dom (h | X) is finite Element of bool X
bool X is non empty finite V60() set
(h | X) | X is Relation-like X -defined X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
rng ((h | X) | X) is finite Element of bool (S1 \/ {x})
bool (S1 \/ {x}) is non empty finite V60() set
rng (h | X) is finite Element of bool (S1 \/ {x})
{ b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( S1[b1,X \/ {S2},S1 \/ {x}] & rng (b1 | X) c= S1 & b1 . S2 = x ) } is set
y is set
c is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
c . S2 is set
c | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
rng (c | X) is finite Element of bool (S1 \/ {x})
bool (S1 \/ {x}) is non empty finite V60() set
dom c is non empty finite Element of bool (X \/ {S2})
bool (X \/ {S2}) is non empty finite V60() set
F1 is set
dom (c | X) is finite Element of bool X
bool X is non empty finite V60() set
F1 is set
(c | X) . F1 is set
c . F1 is set
y is set
c is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
c | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite set
rng (c | X) is finite set
c | X is Relation-like X -defined X \/ {S2} -defined S1 \/ {x} -valued Function-like finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):]
rng (c | X) is finite Element of bool (S1 \/ {x})
bool (S1 \/ {x}) is non empty finite V60() set
c . S2 is set
{ b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : ( b1 is one-to-one & rng (b1 | X) c= S1 ) } is set
F1 is set
F1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:]
F1 | X is Relation-like X -defined X -defined S1 -valued Function-like finite Element of bool [:X,S1:]
rng (F1 | X) is finite Element of bool S1
bool S1 is non empty finite V60() set
rng F1 is finite Element of bool S1
{ b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : S1[b1,X,S1] } is set
card { b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : S1[b1,X,S1] } is V4() V5() V6() cardinal set
card { b1 where b1 is non empty Relation-like X \/ {S2} -defined S1 \/ {x} -valued Function-like V25(X \/ {S2}) quasi_total finite Element of bool [:(X \/ {S2}),(S1 \/ {x}):] : ( S1[b1,X \/ {S2},S1 \/ {x}] & rng (b1 | X) c= S1 & b1 . S2 = x ) } is V4() V5() V6() cardinal set
F1 is set
F1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:]
F1 | X is Relation-like X -defined X -defined S1 -valued Function-like finite Element of bool [:X,S1:]
rng (F1 | X) is finite Element of bool S1
bool S1 is non empty finite V60() set
X is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
X ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
X -' S1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(X -' S1) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(X !) / ((X -' S1) !) is V11() ext-real non negative V53() Element of REAL
X is finite set
card X is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S1 is finite set
card S1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
[:X,S1:] is Relation-like finite set
bool [:X,S1:] is non empty finite V60() set
{ b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : b1 is one-to-one } is set
card { b1 where b1 is Relation-like X -defined S1 -valued Function-like quasi_total finite Element of bool [:X,S1:] : b1 is one-to-one } is V4() V5() V6() cardinal set
(card S1) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card S1) -' (card X) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card S1) -' (card X)) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card S1) !) / (((card S1) -' (card X)) !) is V11() ext-real non negative V53() Element of REAL
S2 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
S2 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
x is finite set
card x is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
h is finite set
card h is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
[:x,h:] is Relation-like finite set
bool [:x,h:] is non empty finite V60() set
{ b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : b1 is one-to-one } is set
card { b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : b1 is one-to-one } is V4() V5() V6() cardinal set
(card h) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card h) -' (card x) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card h) -' (card x)) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card h) !) / (((card h) -' (card x)) !) is V11() ext-real non negative V53() Element of REAL
c is set
F1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:]
rng {} is empty trivial proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() V39() V42() V43() V44() V45() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V201() V205() Element of bool RAT
bool RAT is non empty non trivial non finite set
(card h) - (card x) is V11() ext-real V53() integer Element of INT
dom {} is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() Element of bool NAT
y is set
c is Relation-like Function-like set
dom c is set
rng c is set
[:(card h),h:] is Relation-like finite set
bool [:(card h),h:] is non empty finite V60() set
F1 is Relation-like card h -defined h -valued Function-like quasi_total finite Element of bool [:(card h),h:]
{ b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : S2[b1] } is set
card { b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : S2[b1] } is V4() V5() V6() cardinal set
F1 is V8() Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() V52() finite V205() set
dom F1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of bool NAT
Sum F1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of COMPLEX
S2 ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(S2 !) / (((card h) -' (card x)) !) is V11() ext-real non negative V53() Element of REAL
(card x) - 1 is V11() ext-real V53() integer Element of INT
{y} is non empty trivial finite 1 -element set
x \ {y} is finite Element of bool x
bool x is non empty finite V60() set
(x \ {y}) \/ {y} is non empty finite set
XF is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
XF + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
(XF + 1) - 1 is V11() ext-real V53() integer Element of INT
(S2 + 1) - 1 is V11() ext-real V53() integer Element of INT
XF - XF is V11() ext-real V53() integer Element of INT
S2 - XF is V11() ext-real V53() integer Element of INT
n1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
F1 . n1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
F1 . n1 is set
{(F1 . n1)} is non empty trivial finite 1 -element set
h \ {(F1 . n1)} is finite Element of bool h
bool h is non empty finite V60() set
(h \ {(F1 . n1)}) \/ {(F1 . n1)} is non empty finite set
card (x \ {y}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
card (h \ {(F1 . n1)}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
[:(x \ {y}),(h \ {(F1 . n1)}):] is Relation-like finite set
bool [:(x \ {y}),(h \ {(F1 . n1)}):] is non empty finite V60() set
{ b1 where b1 is Relation-like x \ {y} -defined h \ {(F1 . n1)} -valued Function-like quasi_total finite Element of bool [:(x \ {y}),(h \ {(F1 . n1)}):] : b1 is one-to-one } is set
card { b1 where b1 is Relation-like x \ {y} -defined h \ {(F1 . n1)} -valued Function-like quasi_total finite Element of bool [:(x \ {y}),(h \ {(F1 . n1)}):] : b1 is one-to-one } is V4() V5() V6() cardinal set
(card (h \ {(F1 . n1)})) -' (card (x \ {y})) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card (h \ {(F1 . n1)})) -' (card (x \ {y}))) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(S2 !) / (((card (h \ {(F1 . n1)})) -' (card (x \ {y}))) !) is V11() ext-real non negative V53() Element of REAL
(card x) - (card x) is V11() ext-real V53() integer Element of INT
(card h) - (card x) is V11() ext-real V53() integer Element of INT
(card (h \ {(F1 . n1)})) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
((card (h \ {(F1 . n1)})) + 1) - 1 is V11() ext-real V53() integer Element of INT
(card (x \ {y})) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
((card (x \ {y})) + 1) - 1 is V11() ext-real V53() integer Element of INT
(((card (h \ {(F1 . n1)})) + 1) - 1) - (((card (x \ {y})) + 1) - 1) is V11() ext-real V53() integer Element of INT
{ b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : ( b1 is one-to-one & b1 . y = F1 . n1 ) } is set
card { b1 where b1 is Relation-like x -defined h -valued Function-like quasi_total finite Element of bool [:x,h:] : ( b1 is one-to-one & b1 . y = F1 . n1 ) } is V4() V5() V6() cardinal set
XF is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
F1 . XF is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
len F1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
dom F1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
(len F1) * ((S2 !) / (((card h) -' (card x)) !)) is V11() ext-real non negative V53() Element of REAL
XF is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
F1 . XF is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(S2 + 1) * ((S2 !) / (((card h) -' (card x)) !)) is V11() ext-real non negative V53() Element of REAL
(S2 + 1) * (S2 !) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((S2 + 1) * (S2 !)) / (((card h) -' (card x)) !) is V11() ext-real non negative V53() Element of REAL
S2 is finite set
card S2 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
x is finite set
card x is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
[:S2,x:] is Relation-like finite set
bool [:S2,x:] is non empty finite V60() set
{ b1 where b1 is Relation-like S2 -defined x -valued Function-like quasi_total finite Element of bool [:S2,x:] : b1 is one-to-one } is set
card { b1 where b1 is Relation-like S2 -defined x -valued Function-like quasi_total finite Element of bool [:S2,x:] : b1 is one-to-one } is V4() V5() V6() cardinal set
(card x) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card x) -' (card S2) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card x) -' (card S2)) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card x) !) / (((card x) -' (card S2)) !) is V11() ext-real non negative V53() Element of REAL
(card x) - (card S2) is V11() ext-real V53() integer Element of INT
y is set
c is Relation-like S2 -defined x -valued Function-like quasi_total finite Element of bool [:S2,x:]
dom {} is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() Element of bool NAT
rng {} is empty trivial proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() V39() V42() V43() V44() V45() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V201() V205() Element of bool RAT
bool RAT is non empty non trivial non finite set
X is finite set
[:X,X:] is Relation-like finite set
bool [:X,X:] is non empty finite V60() set
{ b1 where b1 is Relation-like X -defined X -valued Function-like V25(X) quasi_total finite Element of bool [:X,X:] : b1 is Relation-like X -defined X -valued Function-like one-to-one V25(X) quasi_total onto bijective finite Element of bool [:X,X:] } is set
card { b1 where b1 is Relation-like X -defined X -valued Function-like V25(X) quasi_total finite Element of bool [:X,X:] : b1 is Relation-like X -defined X -valued Function-like one-to-one V25(X) quasi_total onto bijective finite Element of bool [:X,X:] } is V4() V5() V6() cardinal set
card X is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(card X) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
{ b1 where b1 is Relation-like X -defined X -valued Function-like V25(X) quasi_total finite Element of bool [:X,X:] : b1 is one-to-one } is set
x is set
h is Relation-like X -defined X -valued Function-like V25(X) quasi_total finite Element of bool [:X,X:]
(card X) -' (card X) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card X) -' (card X)) ! is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
((card X) !) / (((card X) -' (card X)) !) is V11() ext-real non negative V53() Element of REAL
x is set
h is Relation-like X -defined X -valued Function-like V25(X) quasi_total finite Element of bool [:X,X:]
X is finite set
S2 is set
x is set
{S2,x} is non empty finite set
Funcs (X,{S2,x}) is non empty functional finite FUNCTION_DOMAIN of X,{S2,x}
bool (Funcs (X,{S2,x})) is non empty finite V60() set
[:X,{S2,x}:] is Relation-like finite set
bool [:X,{S2,x}:] is non empty finite V60() set
{S2} is non empty trivial finite 1 -element set
S1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
h is set
y is set
c is Relation-like X -defined {S2,x} -valued Function-like V25(X) quasi_total finite Element of bool [:X,{S2,x}:]
c " {S2} is finite Element of bool X
bool X is non empty finite V60() set
card (c " {S2}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
y is functional finite Element of bool (Funcs (X,{S2,x}))
c is set
F1 is Relation-like X -defined {S2,x} -valued Function-like V25(X) quasi_total finite Element of bool [:X,{S2,x}:]
F1 " {S2} is finite Element of bool X
bool X is non empty finite V60() set
card (F1 " {S2}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
h is functional finite Element of bool (Funcs (X,{S2,x}))
y is functional finite Element of bool (Funcs (X,{S2,x}))
c is set
F1 is Relation-like X -defined {S2,x} -valued Function-like V25(X) quasi_total finite Element of bool [:X,{S2,x}:]
F1 " {S2} is finite Element of bool X
bool X is non empty finite V60() set
card (F1 " {S2}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
F1 is Relation-like X -defined {S2,x} -valued Function-like V25(X) quasi_total finite Element of bool [:X,{S2,x}:]
F1 " {S2} is finite Element of bool X
bool X is non empty finite V60() set
card (F1 " {S2}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
X is set
S1 is finite set
card S1 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
S2 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
(S1,S2,X,X) is functional finite Element of bool (Funcs (S1,{X,X}))
{X,X} is non empty finite set
Funcs (S1,{X,X}) is non empty functional finite FUNCTION_DOMAIN of S1,{X,X}
bool (Funcs (S1,{X,X})) is non empty finite V60() set
x is set
[:S1,{X,X}:] is Relation-like finite set
bool [:S1,{X,X}:] is non empty finite V60() set
{X} is non empty trivial finite 1 -element set
h is Relation-like S1 -defined {X,X} -valued Function-like V25(S1) quasi_total finite Element of bool [:S1,{X,X}:]
h " {X} is finite Element of bool S1
bool S1 is non empty finite V60() set
card (h " {X}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
rng h is finite Element of bool {X,X}
bool {X,X} is non empty finite V60() set
dom h is finite Element of bool S1
rng h is finite Element of bool {X,X}
bool {X,X} is non empty finite V60() set
dom h is finite Element of bool S1
rng h is finite Element of bool {X,X}
bool {X,X} is non empty finite V60() set
X is set
S1 is set
S2 is finite set
card S2 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
x is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
(S2,x,X,S1) is functional finite Element of bool (Funcs (S2,{X,S1}))
{X,S1} is non empty finite set
Funcs (S2,{X,S1}) is non empty functional finite FUNCTION_DOMAIN of S2,{X,S1}
bool (Funcs (S2,{X,S1})) is non empty finite V60() set
h is set
[:S2,{X,S1}:] is Relation-like finite set
bool [:S2,{X,S1}:] is non empty finite V60() set
{X} is non empty trivial finite 1 -element set
y is Relation-like S2 -defined {X,S1} -valued Function-like V25(S2) quasi_total finite Element of bool [:S2,{X,S1}:]
y " {X} is finite Element of bool S2
bool S2 is non empty finite V60() set
card (y " {X}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
X is set
S1 is set
S2 is finite set
(S2,0,X,S1) is functional finite Element of bool (Funcs (S2,{X,S1}))
{X,S1} is non empty finite set
Funcs (S2,{X,S1}) is non empty functional finite FUNCTION_DOMAIN of S2,{X,S1}
bool (Funcs (S2,{X,S1})) is non empty finite V60() set
card (S2,0,X,S1) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
dom {} is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() Element of bool NAT
[:S2,{X,S1}:] is Relation-like finite set
bool [:S2,{X,S1}:] is non empty finite V60() set
x is Relation-like S2 -defined {X,S1} -valued Function-like V25(S2) quasi_total finite Element of bool [:S2,{X,S1}:]
{x} is non empty trivial functional finite V60() 1 -element Element of bool (bool [:S2,{X,S1}:])
bool (bool [:S2,{X,S1}:]) is non empty finite V60() set
h is set
{X} is non empty trivial finite 1 -element set
y is Relation-like S2 -defined {X,S1} -valued Function-like V25(S2) quasi_total finite Element of bool [:S2,{X,S1}:]
y " {X} is finite Element of bool S2
bool S2 is non empty finite V60() set
card (y " {X}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
dom y is finite Element of bool S2
{X} is non empty trivial finite 1 -element set
x " {X} is finite Element of bool S2
bool S2 is non empty finite V60() set
card {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() Element of NAT
{S1} is non empty trivial finite 1 -element set
x is Relation-like Function-like set
dom x is set
rng x is set
[:S2,{X,S1}:] is Relation-like finite set
bool [:S2,{X,S1}:] is non empty finite V60() set
{x} is non empty trivial functional finite 1 -element set
h is set
{X} is non empty trivial finite 1 -element set
y is Relation-like S2 -defined {X,S1} -valued Function-like V25(S2) quasi_total finite Element of bool [:S2,{X,S1}:]
y " {X} is finite Element of bool S2
bool S2 is non empty finite V60() set
card (y " {X}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
rng y is finite Element of bool {X,S1}
bool {X,S1} is non empty finite V60() set
dom y is finite Element of bool S2
{X} is non empty trivial finite 1 -element set
x " {X} is set
card {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() Element of NAT
X is set
S1 is set
S2 is finite set
card S2 is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
(S2,(card S2),X,S1) is functional finite Element of bool (Funcs (S2,{X,S1}))
{X,S1} is non empty finite set
Funcs (S2,{X,S1}) is non empty functional finite FUNCTION_DOMAIN of S2,{X,S1}
bool (Funcs (S2,{X,S1})) is non empty finite V60() set
card (S2,(card S2),X,S1) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
dom {} is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V34() V35() V47() V52() V53() integer finite finite-yielding V60() cardinal {} -element Function-yielding V130() V205() Element of bool NAT
[:S2,{X,S1}:] is Relation-like finite set
bool [:S2,{X,S1}:] is non empty finite V60() set
x is Relation-like S2 -defined {X,S1} -valued Function-like V25(S2) quasi_total finite Element of bool [:S2,{X,S1}:]
{x} is non empty trivial functional finite V60() 1 -element Element of bool (bool [:S2,{X,S1}:])
bool (bool [:S2,{X,S1}:]) is non empty finite V60() set
h is set
{X} is non empty trivial finite 1 -element set
y is Relation-like S2 -defined {X,S1} -valued Function-like V25(S2) quasi_total finite Element of bool [:S2,{X,S1}:]
y " {X} is finite Element of bool S2
bool S2 is non empty finite V60() set
card (y " {X}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
dom y is finite Element of bool S2
{X} is non empty trivial finite 1 -element set
x " {X} is finite Element of bool S2
bool S2 is non empty finite V60() set
{X} is non empty trivial finite 1 -element set
x is Relation-like Function-like set
dom x is set
rng x is set
[:S2,{X,S1}:] is Relation-like finite set
bool [:S2,{X,S1}:] is non empty finite V60() set
{x} is non empty trivial functional finite 1 -element set
h is set
y is Relation-like S2 -defined {X,S1} -valued Function-like V25(S2) quasi_total finite Element of bool [:S2,{X,S1}:]
y " {X} is finite Element of bool S2
bool S2 is non empty finite V60() set
card (y " {X}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
rng y is finite Element of bool {X,S1}
bool {X,S1} is non empty finite V60() set
{S1} is non empty trivial finite 1 -element set
y " {S1} is finite Element of bool S2
c is set
y . c is set
rng y is finite Element of bool {X,S1}
bool {X,S1} is non empty finite V60() set
rng y is finite Element of bool {X,S1}
bool {X,S1} is non empty finite V60() set
rng y is finite Element of bool {X,S1}
bool {X,S1} is non empty finite V60() set
dom y is finite Element of bool S2
x " {X} is set
card (x " {X}) is V4() V5() V6() cardinal set
X is set
{X} is non empty trivial finite 1 -element set
S1 is set
{S1} is non empty trivial finite 1 -element set
S2 is set
{S1,S2} is non empty finite set
x is finite set
x \/ {X} is non empty finite set
[:(x \/ {X}),{S1,S2}:] is non empty Relation-like finite set
bool [:(x \/ {X}),{S1,S2}:] is non empty finite V60() set
h is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal set
(x,h,S1,S2) is functional finite Element of bool (Funcs (x,{S1,S2}))
Funcs (x,{S1,S2}) is non empty functional finite FUNCTION_DOMAIN of x,{S1,S2}
bool (Funcs (x,{S1,S2})) is non empty finite V60() set
card (x,h,S1,S2) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
h + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V47() V53() integer finite cardinal Element of NAT
{ b1 where b1 is non empty Relation-like x \/ {X} -defined {S1,S2} -valued Function-like V25(x \/ {X}) quasi_total finite Element of bool [:(x \/ {X}),{S1,S2}:] : ( card (b1 " {S1}) = h + 1 & b1 . X = S1 ) } is set
card { b1 where b1 is non empty Relation-like x \/ {X} -defined {S1,S2} -valued Function-like V25(x \/ {X}) quasi_total finite Element of bool [:(x \/ {X}),{S1,S2}:] : ( card (b1 " {S1}) = h + 1 & b1 . X = S1 ) } is V4() V5() V6() cardinal set
{S1,S2} \/ {S1} is non empty finite set
[:(x \/ {X}),({S1,S2} \/ {S1}):] is non empty Relation-like finite set
bool [:(x \/ {X}),({S1,S2} \/ {S1}):] is non empty finite V60() set
c is non empty Relation-like x \/ {X} -defined {S1,S2} \/ {S1} -valued Function-like V25(x \/ {X}) quasi_total finite Element of bool [:(x \/ {X}),({S1,S2} \/ {S1}):]
c . X is set
c | x is Relation-like x -defined x \/ {X} -defined {S1,S2} \/ {S1} -valued Function-like finite Element of bool [:(x \/ {X}),({S1,S2} \/ {S1}):]
(c | x) | x is Relation-like x -defined x -defined x \/ {X} -defined {S1,S2} \/ {S1} -valued Function-like finite Element of bool [:(x \/ {X}),({S1,S2} \/ {S1}):]
F1 is Relation-like Function-like set
F1 | x is Relation-like Function-like finite set
(F1 | x) " {S1} is finite set
card ((F1 | x) " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
F1 is Relation-like Function-like set
F1 | x is Relation-like Function-like finite set
(F1 | x) " {S1} is finite set
card ((F1 | x) " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
{ b1 where b1 is non empty Relation-like x \/ {X} -defined {S1,S2} \/ {S1} -valued Function-like V25(x \/ {X}) quasi_total finite Element of bool [:(x \/ {X}),({S1,S2} \/ {S1}):] : ( S1[b1,x \/ {X},{S1,S2} \/ {S1}] & rng (b1 | x) c= {S1,S2} & b1 . X = S1 ) } is set
[:x,{S1,S2}:] is Relation-like finite set
bool [:x,{S1,S2}:] is non empty finite V60() set
{ b1 where b1 is Relation-like x -defined {S1,S2} -valued Function-like V25(x) quasi_total finite Element of bool [:x,{S1,S2}:] : S1[b1,x,{S1,S2}] } is set
{S1} \/ {S1,S2} is non empty finite set
{S1,S1,S2} is non empty finite set
F1 is set
XF is non empty Relation-like x \/ {X} -defined {S1,S2} \/ {S1} -valued Function-like V25(x \/ {X}) quasi_total finite Element of bool [:(x \/ {X}),({S1,S2} \/ {S1}):]
XF | x is Relation-like x -defined x \/ {X} -defined {S1,S2} \/ {S1} -valued Function-like finite Element of bool [:(x \/ {X}),({S1,S2} \/ {S1}):]
rng (XF | x) is finite Element of bool ({S1,S2} \/ {S1})
bool ({S1,S2} \/ {S1}) is non empty finite V60() set
XF . X is set
dom XF is non empty finite Element of bool (x \/ {X})
bool (x \/ {X}) is non empty finite V60() set
(x \/ {X}) \ {X} is finite Element of bool (x \/ {X})
(XF | x) " {S1} is finite Element of bool (x \/ {X})
{X} \/ ((XF | x) " {S1}) is non empty finite set
XF " {S1} is finite Element of bool (x \/ {X})
(dom XF) /\ x is finite Element of bool (x \/ {X})
dom (XF | x) is finite Element of bool x
bool x is non empty finite V60() set
card ((XF | x) " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
card (XF " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
F1 is set
XF is Relation-like x -defined {S1,S2} -valued Function-like V25(x) quasi_total finite Element of bool [:x,{S1,S2}:]
XF | x is Relation-like x -defined x -defined {S1,S2} -valued Function-like finite Element of bool [:x,{S1,S2}:]
XF " {S1} is finite Element of bool x
bool x is non empty finite V60() set
card (XF " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
F1 is set
XF is Relation-like x -defined {S1,S2} -valued Function-like V25(x) quasi_total finite Element of bool [:x,{S1,S2}:]
XF " {S1} is finite Element of bool x
bool x is non empty finite V60() set
card (XF " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
dom XF is finite Element of bool x
n is Relation-like Function-like set
n | x is Relation-like Function-like finite set
(n | x) " {S1} is finite set
card ((n | x) " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
card { b1 where b1 is Relation-like x -defined {S1,S2} -valued Function-like V25(x) quasi_total finite Element of bool [:x,{S1,S2}:] : S1[b1,x,{S1,S2}] } is V4() V5() V6() cardinal set
card { b1 where b1 is non empty Relation-like x \/ {X} -defined {S1,S2} \/ {S1} -valued Function-like V25(x \/ {X}) quasi_total finite Element of bool [:(x \/ {X}),({S1,S2} \/ {S1}):] : ( S1[b1,x \/ {X},{S1,S2} \/ {S1}] & rng (b1 | x) c= {S1,S2} & b1 . X = S1 ) } is V4() V5() V6() cardinal set
F1 is set
XF is non empty Relation-like x \/ {X} -defined {S1,S2} -valued Function-like V25(x \/ {X}) quasi_total finite Element of bool [:(x \/ {X}),{S1,S2}:]
XF " {S1} is finite Element of bool (x \/ {X})
bool (x \/ {X}) is non empty finite V60() set
card (XF " {S1}) is V4() V5() V6() V10() V11() ext-real non negative V47() V53() integer finite cardinal Element of NAT
XF . X is set
dom XF is non empty finite Element of bool (x \/ {X})
(dom XF) /\ x is finite Element of bool (x \/ {X})
XF | x is Relation-like x -defined x \/ {X} -defined {S1,S2} -valued Function-like finite Element of bool [:(x \/ {X}),{S1,S2}:]
dom (XF | x) is finite Element of bool x
bool x is non empty finite V60()