:: HALLMAR1 semantic presentation

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

F

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