REAL is set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty 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
{} is set
the empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative finite cardinal Element of NAT
2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative finite cardinal Element of NAT
3 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative finite cardinal Element of NAT
card {} is V4() V5() V6() cardinal set
0 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial finite V39() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{1,2} is finite V39() set
F is finite set
A is finite set
F \/ A is finite set
card (F \/ A) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F /\ A is finite set
card (F /\ A) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card (F \/ A)) + (card (F /\ A)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card F is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card A is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card F) + (card A) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
((card F) + (card A)) - (card (F /\ A)) is V11() V12() ext-real set
F1() is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is V4() V5() V6() V10() V11() V12() ext-real finite cardinal set
F is V4() V5() V6() V10() V11() V12() ext-real finite cardinal set
F + 1 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative finite cardinal Element of NAT
A is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A + 1 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is non empty set
bool F is non empty set
the non empty Element of bool F is non empty Element of bool F
<* the non empty Element of bool F*> is non empty trivial Relation-like NAT -defined bool F -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool F
G is non empty trivial Relation-like NAT -defined bool F -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool F
rng G is non empty trivial finite 1 -element set
{ the non empty Element of bool F} is non empty trivial finite 1 -element set
F is non empty set
bool F is non empty set
A is Relation-like non-empty NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is set
rng A is finite set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is set
dom A is finite Element of bool NAT
dom A is finite Element of bool NAT
dom A is finite Element of bool NAT
F is set
bool F is non empty set
G is set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
i is set
G is set
G is set
A . G is set
rng A is finite set
i is set
G is set
G is set
H is set
l is set
A . H is set
G is set
H is set
l is set
A . H is set
F is set
bool F is non empty set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is set
(F,A,G) is set
i is set
dom A is finite Element of bool NAT
G is set
A . G is set
rng A is finite set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is set
i is set
(F,A,G) is set
(F,A,i) is set
G is set
dom A is finite Element of bool NAT
G is set
A . G is set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is set
(F,A,G) is set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite V39() 1 -element set
(F,A,{G}) is finite set
A . G is finite set
i is set
G is set
A . G is set
i is set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G,i} is finite V39() set
(F,A,{G,i}) is finite set
A . G is finite set
A . i is finite set
(A . G) \/ (A . i) is finite set
G is set
G is set
A . G is set
G is set
F is set
A is finite set
bool A is non empty finite V39() set
G is Relation-like NAT -defined bool A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool A
dom G is finite Element of bool NAT
(A,G,F) is finite set
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . i is finite set
G is set
F is set
A is finite set
bool A is non empty finite V39() set
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite V39() 1 -element set
F \ {G} is Element of bool F
bool F is non empty set
i is Relation-like NAT -defined bool A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool A
dom i is finite Element of bool NAT
(A,i,F) is finite set
(A,i,(F \ {G})) is finite set
i . G is finite set
(A,i,(F \ {G})) \/ (i . G) is finite set
G is set
G is set
i . G is set
G is set
G is set
i . G is set
F is set
A is set
F \/ A is set
G is finite set
bool G is non empty finite V39() set
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{i} is non empty trivial finite V39() 1 -element set
{i} \/ F is set
({i} \/ F) \/ A is set
G is Relation-like NAT -defined bool G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool G
dom G is finite Element of bool NAT
(G,G,(({i} \/ F) \/ A)) is finite set
G . i is finite set
(G,G,(F \/ A)) is finite set
(G . i) \/ (G,G,(F \/ A)) is finite set
(G,G,{i}) is finite set
G is set
l is set
G . l is set
{i} \/ (F \/ A) is set
G is set
l is set
G . l is set
{i} \/ (F \/ A) is set
l is set
G . l is set
{i} \/ (F \/ A) is set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
i is set
G is set
{i} is non empty trivial finite 1 -element set
(A . G) \ {i} is finite Element of bool (A . G)
bool (A . G) is non empty finite V39() set
{G} is non empty trivial finite 1 -element set
(A . G) \ {G} is finite Element of bool (A . G)
((A . G) \ {i}) \/ ((A . G) \ {G}) is finite Element of bool (A . G)
{G} \/ {} is set
{G} \ ({G} \/ {}) is trivial finite Element of bool {G}
bool {G} is non empty finite V39() set
{G} \ {G} is trivial finite Element of bool {G}
(A . G) \ ({G} \ {G}) is finite Element of bool (A . G)
(A . G) /\ {G} is finite set
((A . G) \ {G}) \/ ((A . G) /\ {G}) is finite set
((A . G) \ {G}) \/ {G} is finite set
G is set
((A . G) \ {i}) \/ {i} is finite set
(((A . G) \ {i}) \/ {i}) \/ (((A . G) \ {G}) \/ {G}) is finite set
{G} \/ ((A . G) \ {G}) is finite set
{i} \/ ({G} \/ ((A . G) \ {G})) is finite set
((A . G) \ {i}) \/ ({i} \/ ({G} \/ ((A . G) \ {G}))) is finite set
{i} \/ {G} is finite set
({i} \/ {G}) \/ ((A . G) \ {G}) is finite set
((A . G) \ {i}) \/ (({i} \/ {G}) \/ ((A . G) \ {G})) is finite set
{G} \/ {i} is finite set
((A . G) \ {i}) \/ ({G} \/ {i}) is finite set
(((A . G) \ {i}) \/ ({G} \/ {i})) \/ ((A . G) \ {G}) is finite set
((A . G) \ {i}) \/ {G} is finite set
(((A . G) \ {i}) \/ {G}) \/ {i} is finite set
((((A . G) \ {i}) \/ {G}) \/ {i}) \/ ((A . G) \ {G}) is finite set
{i} \/ ((A . G) \ {G}) is finite set
(((A . G) \ {i}) \/ {G}) \/ ({i} \/ ((A . G) \ {G})) is finite set
((A . G) \ {i}) \/ ({i} \/ ((A . G) \ {G})) is finite set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is set
{i} is non empty trivial finite 1 -element set
A . G is finite set
(A . G) \ {i} is finite Element of bool (A . G)
bool (A . G) is non empty finite V39() set
G is finite Element of bool F
A +* (G,G) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
l is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom l is finite Element of bool NAT
H is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
l . H is finite set
A . H is finite set
(A . H) \ {i} is finite Element of bool (A . H)
bool (A . H) is non empty finite V39() set
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom G is finite Element of bool NAT
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom G is finite Element of bool NAT
l is V4() V5() V6() V10() V11() V12() ext-real finite cardinal set
G . l is set
G . l is set
A . G is finite set
(A . G) \ {i} is finite Element of bool (A . G)
bool (A . G) is non empty finite V39() set
A . l is set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
card (A . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card (A . G)) - 1 is V11() V12() ext-real set
i is set
(F,A,G,i) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
(F,A,G,i) . G is finite set
card ((F,A,G,i) . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
dom (F,A,G,i) is finite Element of bool NAT
{i} is non empty trivial finite 1 -element set
(A . G) \ {i} is finite Element of bool (A . G)
bool (A . G) is non empty finite V39() set
card {i} is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card (A . G)) - (card {i}) is V11() V12() ext-real set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite V39() 1 -element set
i is set
(F,A,G,i) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is set
G \ {G} is Element of bool G
bool G is non empty set
(F,(F,A,G,i),(G \ {G})) is finite set
(F,A,(G \ {G})) is finite set
G is set
dom (F,A,G,i) is finite Element of bool NAT
l is set
(F,A,G,i) . l is set
A . l is set
dom A is finite Element of bool NAT
dom (F,A,G,i) is finite Element of bool NAT
dom A is finite Element of bool NAT
G is set
l is set
A . l is set
(F,A,G,i) . l is set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is set
(F,A,G) is finite set
i is set
(F,A,G,i) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
(F,(F,A,G,i),G) is finite set
G is set
dom A is finite Element of bool NAT
l is set
A . l is set
dom (F,A,G,i) is finite Element of bool NAT
(F,A,G,i) . l is set
G is set
dom (F,A,G,i) is finite Element of bool NAT
l is set
(F,A,G,i) . l is set
dom A is finite Element of bool NAT
A . l is set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite V39() 1 -element set
A . G is finite set
i is set
(F,A,G,i) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom (F,A,G,i) is finite Element of bool NAT
G is set
(F,(F,A,G,i),G) is finite set
G \ {G} is Element of bool G
bool G is non empty set
(F,A,(G \ {G})) is finite set
{i} is non empty trivial finite 1 -element set
(A . G) \ {i} is finite Element of bool (A . G)
bool (A . G) is non empty finite V39() set
(F,A,(G \ {G})) \/ ((A . G) \ {i}) is finite set
(F,(F,A,G,i),(G \ {G})) is finite set
(F,A,G,i) . G is finite set
(F,(F,A,G,i),(G \ {G})) \/ ((F,A,G,i) . G) is finite set
(F,A,(G \ {G})) \/ ((F,A,G,i) . G) is finite set
F is finite set
bool F is non empty finite V39() set
F is finite set
bool F is non empty finite V39() set
F is non empty finite set
bool F is non empty finite V39() set
the Element of F is Element of F
{ the Element of F} is non empty trivial finite 1 -element set
G is finite Element of bool F
<*G*> is non empty trivial Relation-like NAT -defined bool F -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool F
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom i is finite Element of bool NAT
G is finite set
card G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,i,G) is finite set
card (F,i,G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,i,{1}) is finite set
i . 1 is finite set
F is finite set
bool F is non empty finite V39() set
<*> (bool F) is empty proper V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined bool F -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of bool F
[:NAT,(bool F):] is non empty non trivial Relation-like non finite set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is finite set
card G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,G) is finite set
card (F,A,G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
rng A is non empty finite set
dom A is non empty finite Element of bool NAT
G is set
A . G is set
{G} is non empty trivial finite 1 -element set
card {G} is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,{G}) is finite set
card (F,A,{G}) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
card (A . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite V39() 1 -element set
card {G} is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,{G}) is finite set
card (F,A,{G}) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is non empty finite Element of bool NAT
G is non empty set
i is Element of G
A . i is set
the Element of A . i is Element of A . i
rng A is non empty finite set
[:G,F:] is non empty Relation-like set
bool [:G,F:] is non empty set
i is Relation-like G -defined F -valued Function-like V30(G,F) Element of bool [:G,F:]
i is Relation-like G -defined F -valued Function-like V30(G,F) Element of bool [:G,F:]
dom i is set
rng i is set
G is set
rng A is non empty finite set
G is set
i . G is set
A . G is set
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal set
Seg G is finite G -element Element of bool NAT
G is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F
dom G is finite Element of bool NAT
{{}} is non empty trivial finite 1 -element set
card {{}} is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
l is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . G is set
G . l is set
A . G is finite set
card (A . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
H is set
{H} is non empty trivial finite 1 -element set
{(G . G)} is non empty trivial finite 1 -element set
JJ2 is set
JJ2 is set
A . l is finite set
card (A . l) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
JJ2 is set
{JJ2} is non empty trivial finite 1 -element set
{(G . l)} is non empty trivial finite 1 -element set
J2 is set
J2 is set
{G,l} is finite V39() set
{(G . G),(G . l)} is finite set
card {G,l} is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,{G,l}) is finite set
card (F,A,{G,l}) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(A . G) \/ (A . l) is finite set
card ((A . G) \/ (A . l)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card {(G . G),(G . l)} is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is set
l is set
G . G is set
G . l is set
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . G is set
A . G is finite set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is set
dom A is finite Element of bool NAT
i is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F
dom i is finite Element of bool NAT
G is finite set
card G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,G) is finite set
card (F,A,G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i | G is Relation-like NAT -defined G -defined NAT -defined F -valued Function-like finite FinSubsequence-like set
dom (i | G) is finite set
rng (i | G) is finite set
JJ2 is set
J2 is set
(i | G) . J2 is set
L is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i . L is set
A . L is finite set
(i | G) . L is set
F is set
bool F is non empty set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is set
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . i is set
F is set
bool F is non empty set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is set
F is set
bool F is non empty set
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
A . G is set
the Element of A . G is Element of A . G
{ the Element of A . G} is non empty trivial finite 1 -element set
G is Element of bool F
A +* (G,G) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
l is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . l is set
A . l is set
G . G is set
G . G is set
card (G . G) is V4() V5() V6() cardinal set
dom G is finite Element of bool NAT
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G)
dom i is finite Element of bool NAT
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i . G is finite set
A . G is finite set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is set
(F,A,G,i) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom (F,A,G,i) is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
(F,A,G,i) . G is finite set
(F,A,G,i) . G is finite set
A . G is finite set
{i} is non empty trivial finite 1 -element set
(A . G) \ {i} is finite Element of bool (A . G)
bool (A . G) is non empty finite V39() set
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is set
(F,A,G,i) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,G)
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i . G is finite set
A . G is finite set
dom G is finite Element of bool NAT
G . G is finite set
dom G is finite Element of bool NAT
dom i is finite Element of bool NAT
F is non empty finite set
bool F is non empty finite V39() set
A is Relation-like non-empty NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G)
i . G is finite set
A . G is finite set
F is non empty finite set
bool F is non empty finite V39() set
A is Relation-like non-empty NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G)
G . i is finite set
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,G,i)
G . G is finite set
dom G is finite Element of bool NAT
G . G is finite set
A . G is finite set
card (G . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card (G . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . i is finite set
G . i is finite set
card (G . i) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is set
bool F is non empty set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
dom A is finite Element of bool NAT
A . G is set
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . i is set
F is set
bool F is non empty set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is set
F is non empty set
bool F is non empty set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is set
A . G is set
choose (A . G) is Element of A . G
{(choose (A . G))} is non empty trivial finite 1 -element set
[:(dom A),(bool F):] is Relation-like set
bool [:(dom A),(bool F):] is non empty set
G is Relation-like dom A -defined bool F -valued Function-like V30( dom A, bool F) finite Element of bool [:(dom A),(bool F):]
G is Relation-like dom A -defined bool F -valued Function-like V30( dom A, bool F) finite Element of bool [:(dom A),(bool F):]
dom G is finite set
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . i is set
A . i is set
choose (A . i) is Element of A . i
{(choose (A . i))} is non empty trivial finite 1 -element set
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . i is set
A . i is set
choose (A . i) is Element of A . i
{(choose (A . i))} is non empty trivial finite 1 -element set
len A is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
Seg (len A) is finite len A -element Element of bool NAT
rng G is finite set
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i . G is set
card (i . G) is V4() V5() V6() cardinal set
dom i is finite Element of bool NAT
A . G is set
choose (A . G) is Element of A . G
{(choose (A . G))} is non empty trivial finite 1 -element set
F is non empty finite set
bool F is non empty finite V39() set
A is non empty Relation-like non-empty NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is non empty finite Element of bool NAT
G is Relation-like Function-like set
dom G is set
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i . G is finite set
card (i . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i . G is finite set
A . G is finite set
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . G is finite set
card (G . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
F is non empty finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G)
dom i is finite Element of bool NAT
dom A is non empty finite Element of bool NAT
F is non empty finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
dom G is finite Element of bool NAT
dom A is non empty finite Element of bool NAT
F is non empty finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is set
i is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
dom i is finite Element of bool NAT
G is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F
dom G is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . G is set
A . G is finite set
i . G is finite set
dom A is non empty finite Element of bool NAT
dom A is non empty finite Element of bool NAT
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
card (A . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is non trivial finite set
G is set
G is set
(F,A,G,G) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom (F,A,G,G) is finite Element of bool NAT
l is finite set
card l is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,(F,A,G,G),l) is finite set
card (F,(F,A,G,G),l) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite 1 -element set
(A . G) \ {G} is finite Element of bool (A . G)
bool (A . G) is non empty finite V39() set
{G} is non empty trivial finite V39() 1 -element set
l \ {G} is finite Element of bool l
bool l is non empty finite V39() set
card (l \ {G}) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card {G} is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card l) - (card {G}) is V11() V12() ext-real set
(card l) - 1 is V11() V12() ext-real set
(F,A,(l \ {G})) is finite set
(F,A,(l \ {G})) \/ ((A . G) \ {G}) is finite set
card ((F,A,(l \ {G})) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
H is finite set
(F,A,H) is finite set
(F,A,H) \/ ((A . G) \ {G}) is finite set
card ((F,A,H) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card H is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
dom A is finite Element of bool NAT
card (F,A,H) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
H is finite set
(F,A,H) is finite set
(F,A,H) \/ ((A . G) \ {G}) is finite set
card ((F,A,H) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card H is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
H is finite set
(F,A,H) is finite set
(F,A,H) \/ ((A . G) \ {G}) is finite set
card ((F,A,H) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card H is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,G,G) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom (F,A,G,G) is finite Element of bool NAT
JJ2 is finite set
card JJ2 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,(F,A,G,G),JJ2) is finite set
card (F,(F,A,G,G),JJ2) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite 1 -element set
(A . G) \ {G} is finite Element of bool (A . G)
{G} is non empty trivial finite V39() 1 -element set
JJ2 \ {G} is finite Element of bool JJ2
bool JJ2 is non empty finite V39() set
card (JJ2 \ {G}) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card {G} is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card JJ2) - (card {G}) is V11() V12() ext-real set
(card JJ2) - 1 is V11() V12() ext-real set
(F,A,(JJ2 \ {G})) is finite set
(F,A,(JJ2 \ {G})) \/ ((A . G) \ {G}) is finite set
card ((F,A,(JJ2 \ {G})) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,JJ2) is finite set
(F,A,JJ2) \/ ((A . G) \ {G}) is finite set
card ((F,A,JJ2) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
dom A is finite Element of bool NAT
card (F,A,JJ2) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
J2 is finite set
(F,A,J2) is finite set
(F,A,J2) \/ ((A . G) \ {G}) is finite set
card ((F,A,J2) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card J2 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
J2 is finite set
(F,A,J2) is finite set
(F,A,J2) \/ ((A . G) \ {G}) is finite set
card ((F,A,J2) \/ ((A . G) \ {G})) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card J2 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} is non empty trivial finite V39() 1 -element set
H \/ J2 is finite set
{G} \/ (H \/ J2) is finite set
dom A is finite Element of bool NAT
(F,A,(H \/ J2)) is finite set
(F,A,(H \/ J2)) \/ i is non trivial finite set
i \ {G} is finite Element of bool i
bool i is non empty finite V39() set
(F,A,H) \/ (i \ {G}) is finite set
i \ {G} is finite Element of bool i
(F,A,J2) \/ (i \ {G}) is finite set
((F,A,H) \/ (i \ {G})) \/ ((F,A,J2) \/ (i \ {G})) is finite set
S2 is set
S1 is set
A . S1 is set
(F,A,H) \/ (F,A,J2) is finite set
(i \ {G}) \/ (i \ {G}) is finite Element of bool i
((F,A,H) \/ (F,A,J2)) \/ ((i \ {G}) \/ (i \ {G})) is finite set
((F,A,H) \/ (F,A,J2)) \/ (i \ {G}) is finite set
(((F,A,H) \/ (F,A,J2)) \/ (i \ {G})) \/ (i \ {G}) is finite set
((F,A,H) \/ (i \ {G})) \/ (F,A,J2) is finite set
(((F,A,H) \/ (i \ {G})) \/ (F,A,J2)) \/ (i \ {G}) is finite set
(i \ {G}) \/ (i \ {G}) is finite Element of bool i
((i \ {G}) \/ (i \ {G})) \/ (F,A,H) is finite set
(((i \ {G}) \/ (i \ {G})) \/ (F,A,H)) \/ (F,A,J2) is finite set
(F,A,H) \/ (F,A,J2) is finite set
((F,A,H) \/ (F,A,J2)) \/ ((i \ {G}) \/ (i \ {G})) is finite set
((F,A,H) \/ (F,A,J2)) \/ (i \ {G}) is finite set
(((F,A,H) \/ (F,A,J2)) \/ (i \ {G})) \/ (i \ {G}) is finite set
((F,A,H) \/ (i \ {G})) \/ (F,A,J2) is finite set
(((F,A,H) \/ (i \ {G})) \/ (F,A,J2)) \/ (i \ {G}) is finite set
card ((F,A,(H \/ J2)) \/ i) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card (((F,A,H) \/ (i \ {G})) \/ ((F,A,J2) \/ (i \ {G}))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
H /\ J2 is finite set
(F,A,(H /\ J2)) is finite set
(F,A,H) /\ (F,A,J2) is finite set
S2 is set
S1 is set
A . S1 is set
card (F,A,(H /\ J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card ((F,A,H) /\ (F,A,J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i \/ (F,A,(H \/ J2)) is non trivial finite set
card (i \/ (F,A,(H \/ J2))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card (i \/ (F,A,(H \/ J2)))) + (card (F,A,(H /\ J2))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card ((F,A,(H \/ J2)) \/ i)) + (card ((F,A,H) /\ (F,A,J2))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
L is finite set
card ({G} \/ (H \/ J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(F,A,({G} \/ (H \/ J2))) is finite set
card (F,A,({G} \/ (H \/ J2))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
{G} \/ H is finite set
({G} \/ H) \/ J2 is finite set
(F,A,(({G} \/ H) \/ J2)) is finite set
card (F,A,(({G} \/ H) \/ J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card {G} is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card (H \/ J2) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card {G}) + (card (H \/ J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
card (H /\ J2) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card ((F,A,H) \/ ((A . G) \ {G}))) + (card ((F,A,J2) \/ ((A . G) \ {G}))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card H) + (card J2) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
((F,A,H) \/ (i \ {G})) /\ ((F,A,J2) \/ (i \ {G})) is finite set
card (((F,A,H) \/ (i \ {G})) /\ ((F,A,J2) \/ (i \ {G}))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card (((F,A,H) \/ (i \ {G})) \/ ((F,A,J2) \/ (i \ {G})))) + (card (((F,A,H) \/ (i \ {G})) /\ ((F,A,J2) \/ (i \ {G})))) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
a is set
1 + (card (H \/ J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(1 + (card (H \/ J2))) + (card (H /\ J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(card (H \/ J2)) + (card (H /\ J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
1 + ((card H) + (card J2)) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is finite set
bool F is non empty finite V39() set
A is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
A . G is finite set
card (A . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G + 1 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
G . G is finite set
card (G . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
G . G is finite set
card (G . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative finite cardinal Element of NAT
l is set
(F,G,G,l) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom G is finite Element of bool NAT
(F,G,G,l) . G is finite set
card ((F,G,G,l) . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
(G + 1) - 1 is V11() V12() ext-real set
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
G . G is finite set
card (G . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
G . G is finite set
card (G . G) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
dom A is non empty finite Element of bool NAT
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G + 1 is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G + 1)
G is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
i is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G)
i is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G)
dom i is non empty finite Element of bool NAT
G is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,i,G + 1)
dom G is non empty finite Element of bool NAT
G . G is finite set
i . (G + 1) is finite set
G is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G + 1)
l is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
len A is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . l is finite set
i is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A,G + 1)
G is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A, 0 )
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
len A is non empty V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A, len A)
G is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A, len A)
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
dom G is non empty finite Element of bool NAT
F is non empty finite set
bool F is non empty finite V39() set
A is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
G is set
G is non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like (F,A)
dom G is non empty finite Element of bool NAT
i is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
G . i is finite set
card (G . i) is V4() V5() V6() V10() V11() V12() ext-real finite cardinal Element of NAT
dom A is non empty finite Element of bool NAT
i is set