:: STACKS_1 semantic presentation

REAL is set

NAT is non empty V39() V40() V41() V46() V51() V52() Element of bool REAL

bool REAL is non empty set

NAT is non empty V39() V40() V41() V46() V51() V52() set

bool NAT is non empty V46() set

bool NAT is non empty V46() set

1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

2 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() set

{{},1} is non empty set

K439() is set

bool K439() is non empty set

K440() is Element of bool K439()

K480() is non empty V221() L22()

the carrier of K480() is non empty set

K443( the carrier of K480()) is non empty M32( the carrier of K480())

K479(K480()) is Element of bool K443( the carrier of K480())

bool K443( the carrier of K480()) is non empty set

[:K479(K480()),NAT:] is Relation-like set

bool [:K479(K480()),NAT:] is non empty set

[:NAT,K479(K480()):] is Relation-like set

bool [:NAT,K479(K480()):] is non empty set

K532() is set

bool K532() is non empty set

[:K532(),NAT:] is Relation-like set

bool [:K532(),NAT:] is non empty set

K534() is M16(K532())

K536() is set

K537() is set

K538() is set

K89(K536(),K537(),K538()) is non empty set

[:K534(),NAT:] is Relation-like set

K579() is non empty V204() V206() V207() V208() L21()

the carrier of K579() is non empty set

COMPLEX is set

RAT is set

INT is set

[:NAT,REAL:] is Relation-like set

bool [:NAT,REAL:] is non empty set

K278(1,NAT) is M16( NAT )

3 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() Element of NAT

X is set

G is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of X

c

G ^ c

X * is functional non empty FinSequence-membered M16(X)

G ^ c

X is set

G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

c

Del (c

X * is functional non empty FinSequence-membered M16(X)

rng (Del (c

rng c

bool X is non empty set

X is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

Del ({},X) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set

dom (Del ({},X)) is Element of bool NAT

dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() Element of bool NAT

F

<*> F

[:NAT,F

X is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

X + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

G is Relation-like NAT -defined F

len G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X2 is Element of F

<*X2*> is Relation-like NAT -defined F

[1,X2] is set

{1,X2} is non empty set

{1} is non empty trivial V53(1) set

{{1,X2},{1}} is non empty set

{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set

c

(F

F

len c

(len c

X is Relation-like NAT -defined F

len X is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

G is Relation-like NAT -defined F

len G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X is non empty set

G is non empty set

[:X,G:] is Relation-like non empty set

[:[:X,G:],G:] is Relation-like non empty set

bool [:[:X,G:],G:] is non empty set

c

pr2 (X,G) is Relation-like [:X,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:X,G:],G:]

X2 is Relation-like [:X,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:X,G:],G:]

A is Element of X

s1 is Element of G

s2 is Element of G

[s1,s2] is Element of [:G,G:]

[:G,G:] is Relation-like non empty set

{s1,s2} is non empty set

{s1} is non empty trivial V53(1) set

{{s1,s2},{s1}} is non empty set

X2 . (A,s1) is Element of G

[A,s1] is set

{A,s1} is non empty set

{A} is non empty trivial V53(1) set

{{A,s1},{A}} is non empty set

X2 . [A,s1] is set

X2 . (A,s2) is Element of G

[A,s2] is set

{A,s2} is non empty set

{{A,s2},{A}} is non empty set

X2 . [A,s2] is set

[(X2 . (A,s1)),(X2 . (A,s2))] is Element of [:G,G:]

{(X2 . (A,s1)),(X2 . (A,s2))} is non empty set

{(X2 . (A,s1))} is non empty trivial V53(1) set

{{(X2 . (A,s1)),(X2 . (A,s2))},{(X2 . (A,s1))}} is non empty set

F

F

F

[:F

[:[:F

bool [:[:F

X is Relation-like [:F

dom X is Relation-like F

bool [:F

rng X is set

G is set

c

X . c

X2 is set

A is set

[X2,A] is set

{X2,A} is non empty set

{X2} is non empty trivial V53(1) set

{{X2,A},{X2}} is non empty set

X . (X2,A) is set

X . [X2,A] is set

F

G is Relation-like [:F

c

X2 is Element of F

G . (c

[c

{c

{c

{{c

G . [c

F

G is non empty set

[:G,G:] is Relation-like non empty set

bool [:G,G:] is non empty set

X is non empty set

[:X,G:] is Relation-like non empty set

[:[:X,G:],G:] is Relation-like non empty set

bool [:[:X,G:],G:] is non empty set

X2 is Relation-like [:X,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:X,G:],G:]

c

Class c

[:X,(Class c

[:[:X,(Class c

bool [:[:X,(Class c

A is set

s1 is set

Class (c

bool G is non empty set

{s1} is non empty trivial V53(1) set

c

A is Relation-like Function-like set

dom A is set

rng A is set

s1 is set

s2 is set

A . s2 is set

bool G is non empty set

[:G,(Class c

bool [:G,(Class c

s1 is Relation-like G -defined Class c

[:(Class c

bool [:(Class c

s2 is Relation-like Class c

e1 is Relation-like [:X,(Class c

e2 is set

q2 is set

e1 is set

e1 . (e2,q2) is set

[e2,q2] is set

{e2,q2} is non empty set

{e2} is non empty trivial V53(1) set

{{e2,q2},{e2}} is non empty set

e1 . [e2,q2] is set

X2 . (e2,e1) is set

[e2,e1] is set

{e2,e1} is non empty set

{{e2,e1},{e2}} is non empty set

X2 . [e2,e1] is set

Class (c

{(X2 . (e2,e1))} is non empty trivial V53(1) set

c

e3 is Element of Class c

s2 . e3 is Element of G

a is Element of G

[(s2 . e3),a] is Element of [:G,G:]

{(s2 . e3),a} is non empty set

{(s2 . e3)} is non empty trivial V53(1) set

{{(s2 . e3),a},{(s2 . e3)}} is non empty set

v is set

Class (c

{v} is non empty trivial V53(1) set

c

e2 is Element of X

X2 . (e2,(s2 . e3)) is Element of G

[e2,(s2 . e3)] is set

{e2,(s2 . e3)} is non empty set

{e2} is non empty trivial V53(1) set

{{e2,(s2 . e3)},{e2}} is non empty set

X2 . [e2,(s2 . e3)] is set

X2 . (e2,a) is Element of G

[e2,a] is set

{e2,a} is non empty set

{{e2,a},{e2}} is non empty set

X2 . [e2,a] is set

[(X2 . (e2,(s2 . e3))),(X2 . (e2,a))] is Element of [:G,G:]

{(X2 . (e2,(s2 . e3))),(X2 . (e2,a))} is non empty set

{(X2 . (e2,(s2 . e3)))} is non empty trivial V53(1) set

{{(X2 . (e2,(s2 . e3))),(X2 . (e2,a))},{(X2 . (e2,(s2 . e3)))}} is non empty set

EqClass (c

{(X2 . (e2,a))} is non empty trivial V53(1) set

c

s1 . (X2 . (e2,(s2 . e3))) is Element of Class c

EqClass (c

c

e1 . (e2,e3) is Element of Class c

[e2,e3] is set

{e2,e3} is non empty set

{{e2,e3},{e2}} is non empty set

e1 . [e2,e3] is set

A is Relation-like [:X,(Class c

s1 is Relation-like [:X,(Class c

bool G is non empty set

e1 is Element of Class c

e2 is set

Class (c

{e2} is non empty trivial V53(1) set

c

s2 is Element of X

A . (s2,e1) is Element of Class c

[s2,e1] is set

{s2,e1} is non empty set

{s2} is non empty trivial V53(1) set

{{s2,e1},{s2}} is non empty set

A . [s2,e1] is set

X2 . (s2,e2) is set

[s2,e2] is set

{s2,e2} is non empty set

{{s2,e2},{s2}} is non empty set

X2 . [s2,e2] is set

Class (c

{(X2 . (s2,e2))} is non empty trivial V53(1) set

c

s1 . (s2,e1) is Element of Class c

s1 . [s2,e1] is set

X is non empty set

bool X is non empty set

G is non empty set

bool G is non empty set

[:X,G:] is Relation-like non empty set

bool [:X,G:] is non empty set

c

X2 is Element of bool G

[:c

bool [:c

A is Relation-like X -defined G -valued Function-like non empty total quasi_total Element of bool [:X,G:]

s1 is Relation-like c

A +* s1 is Relation-like Function-like non empty set

A +* {} is Relation-like Function-like non empty set

dom (A +* s1) is non empty set

dom A is non empty Element of bool X

dom s1 is Element of bool c

bool c

(dom A) \/ (dom s1) is non empty set

X \/ (dom s1) is non empty set

X \/ c

rng (A +* s1) is non empty set

rng A is non empty Element of bool G

rng s1 is Element of bool X2

bool X2 is non empty set

(rng A) \/ (rng s1) is non empty set

G \/ X2 is non empty set

G is set

bool G is non empty set

X is non empty set

[:X,G:] is Relation-like set

[:[:X,G:],G:] is Relation-like set

bool [:[:X,G:],G:] is non empty set

[:G,G:] is Relation-like set

bool [:G,G:] is non empty set

[:G,X:] is Relation-like set

bool [:G,X:] is non empty set

c

X2 is Relation-like [:X,G:] -defined G -valued Function-like quasi_total Element of bool [:[:X,G:],G:]

A is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s1 is Relation-like G -defined X -valued Function-like total quasi_total Element of bool [:G,X:]

(X,G,c

G is non empty set

bool G is non empty set

X is set

[:X,G:] is Relation-like set

[:[:X,G:],G:] is Relation-like set

bool [:[:X,G:],G:] is non empty set

[:G,G:] is Relation-like non empty set

bool [:G,G:] is non empty set

[:G,X:] is Relation-like set

bool [:G,X:] is non empty set

c

X2 is Relation-like [:X,G:] -defined G -valued Function-like total quasi_total Element of bool [:[:X,G:],G:]

A is Relation-like G -defined G -valued Function-like non empty total quasi_total Element of bool [:G,G:]

s1 is Relation-like G -defined X -valued Function-like quasi_total Element of bool [:G,X:]

(X,G,c

the non empty set is non empty set

bool the non empty set is non empty set

the Element of bool the non empty set is Element of bool the non empty set

[: the non empty set , the non empty set :] is Relation-like non empty set

[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like non empty set

bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set

the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :]

bool [: the non empty set , the non empty set :] is non empty set

the Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :] is Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :]

( the non empty set , the non empty set , the Element of bool the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :], the Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :]) is non empty non void V67() () ()

X is ()

the carrier' of X is set

X is non void ()

the carrier' of X is non empty set

the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]

[: the carrier' of X, the carrier' of X:] is Relation-like non empty set

bool [: the carrier' of X, the carrier' of X:] is non empty set

G is Element of the carrier' of X

the of X . G is Element of the carrier' of X

the carrier of X is set

the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier' of X, the carrier of X:]

[: the carrier' of X, the carrier of X:] is Relation-like set

bool [: the carrier' of X, the carrier of X:] is non empty set

the of X . G is Element of the carrier of X

X is non empty non void V67() ()

the carrier' of X is non empty set

the carrier of X is non empty set

the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]

[: the carrier of X, the carrier' of X:] is Relation-like non empty set

[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set

bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set

c

G is Element of the carrier' of X

the of X . (c

[c

{c

{c

{{c

the of X . [c

X is non empty set

X * is functional non empty FinSequence-membered M16(X)

<*> X is Relation-like non-empty empty-yielding NAT -defined X -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() FinSequence of X

[:NAT,X:] is Relation-like non empty V46() set

G is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

{G} is functional non empty trivial V53(1) FinSequence-membered Element of bool (X *)

bool (X *) is non empty set

the Element of X is Element of X

[:X,(X *):] is Relation-like non empty set

[:[:X,(X *):],(X *):] is Relation-like non empty set

bool [:[:X,(X *):],(X *):] is non empty set

X2 is Relation-like [:X,(X *):] -defined X * -valued Function-like non empty total quasi_total Element of bool [:[:X,(X *):],(X *):]

[:(X *),(X *):] is Relation-like non empty set

bool [:(X *),(X *):] is non empty set

A is Relation-like X * -defined X * -valued Function-like non empty total quasi_total Element of bool [:(X *),(X *):]

[:(X *),X:] is Relation-like non empty set

bool [:(X *),X:] is non empty set

s1 is Relation-like X * -defined X -valued Function-like non empty total quasi_total Element of bool [:(X *),X:]

(X,(X *),{G},X2,A,s1) is non empty non void V67() () ()

s2 is non empty non void V67() () ()

the carrier of s2 is non empty set

the carrier' of s2 is non empty set

the Element of the carrier of s2 is Element of the carrier of s2

e1 is Element of the carrier' of s2

(s2,e1) is Element of the carrier of s2

the of s2 is Relation-like the carrier' of s2 -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of s2, the carrier of s2:]

[: the carrier' of s2, the carrier of s2:] is Relation-like non empty set

bool [: the carrier' of s2, the carrier of s2:] is non empty set

the of s2 . e1 is Element of the carrier of s2

(s2,e1) is Element of the carrier' of s2

the of s2 is Relation-like the carrier' of s2 -defined the carrier' of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of s2, the carrier' of s2:]

[: the carrier' of s2, the carrier' of s2:] is Relation-like non empty set

bool [: the carrier' of s2, the carrier' of s2:] is non empty set

the of s2 . e1 is Element of the carrier' of s2

e2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set

e2 . 1 is set

Del (e2,1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set

q2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

dom q2 is Element of bool NAT

q2 /. 1 is Element of X

IFEQ (e1,{}, the Element of X,(q2 /. 1)) is Element of X

e1 is Element of the carrier of s2

(s2,e1,e1) is Element of the carrier' of s2

the of s2 is Relation-like [: the carrier of s2, the carrier' of s2:] -defined the carrier' of s2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:]

[: the carrier of s2, the carrier' of s2:] is Relation-like non empty set

[:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:] is Relation-like non empty set

bool [:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:] is non empty set

the of s2 . (e1,e1) is Element of the carrier' of s2

[e1,e1] is set

{e1,e1} is non empty set

{e1} is non empty trivial V53(1) set

{{e1,e1},{e1}} is non empty set

the of s2 . [e1,e1] is set

<*e1*> is Relation-like NAT -defined the carrier of s2 -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of s2

[1,e1] is set

{1,e1} is non empty set

{1} is non empty trivial V53(1) set

{{1,e1},{1}} is non empty set

{[1,e1]} is Relation-like Function-like constant non empty trivial V53(1) set

<*e1*> ^ e2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set

G is non empty non void V67() () ()

the carrier of G is non empty set

the carrier' of G is non empty set

the Element of the carrier of G is Element of the carrier of G

c

the carrier of c

the carrier' of c

the Element of the carrier of c

X2 is Element of X

s2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

the of G is Relation-like [: the carrier of G, the carrier' of G:] -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:]

[: the carrier of G, the carrier' of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier' of G:], the carrier' of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:] is non empty set

the of G . (X2,s2) is set

[X2,s2] is set

{X2,s2} is non empty set

{X2} is non empty trivial V53(1) set

{{X2,s2},{X2}} is non empty set

the of G . [X2,s2] is set

e1 is Element of the carrier' of G

A is Element of the carrier of G

(G,e1,A) is Element of the carrier' of G

the of G . (A,e1) is Element of the carrier' of G

[A,e1] is set

{A,e1} is non empty set

{A} is non empty trivial V53(1) set

{{A,e1},{A}} is non empty set

the of G . [A,e1] is set

<*X2*> is Relation-like NAT -defined X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of X

[1,X2] is set

{1,X2} is non empty set

{1} is non empty trivial V53(1) set

{{1,X2},{1}} is non empty set

{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set

(X,<*X2*>,s2) is Relation-like NAT -defined X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of X *

e2 is Element of the carrier' of c

s1 is Element of the carrier of c

(c

the of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the of c

[s1,e2] is set

{s1,e2} is non empty set

{s1} is non empty trivial V53(1) set

{{s1,e2},{s1}} is non empty set

the of c

the of c

the of c

X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

A is Element of the carrier' of G

s1 is Element of the carrier' of c

the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]

[: the carrier' of G, the carrier' of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier' of G:] is non empty set

the of G . X2 is set

(G,A) is Element of the carrier' of G

the of G . A is Element of the carrier' of G

(X,1,X2) is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

(c

the of c

[: the carrier' of c

bool [: the carrier' of c

the of c

the of c

A is Element of the carrier' of G

s1 is Element of the carrier' of c

the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]

[: the carrier' of G, the carrier' of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier' of G:] is non empty set

the of G . X2 is set

(G,A) is Element of the carrier' of G

the of G . A is Element of the carrier' of G

(c

the of c

[: the carrier' of c

bool [: the carrier' of c

the of c

the of c

A is Element of the carrier' of G

the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]

[: the carrier' of G, the carrier' of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier' of G:] is non empty set

the of c

[: the carrier' of c

bool [: the carrier' of c

the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]

[: the carrier' of G, the carrier' of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier' of G:] is non empty set

the of c

[: the carrier' of c

bool [: the carrier' of c

X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

A is Element of the carrier' of G

s1 is Element of the carrier' of c

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

[: the carrier' of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier of G:] is non empty set

the of G . X2 is set

(G,A) is Element of the carrier of G

the of G . A is Element of the carrier of G

X2 . 1 is set

(c

the of c

[: the carrier' of c

bool [: the carrier' of c

the of c

the of c

A is Element of the carrier' of G

s1 is Element of the carrier' of c

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

[: the carrier' of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier of G:] is non empty set

the of G . X2 is set

(G,A) is Element of the carrier of G

the of G . A is Element of the carrier of G

the Element of X is Element of X

(c

the of c

[: the carrier' of c

bool [: the carrier' of c

the of c

the of c

A is Element of the carrier' of G

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

[: the carrier' of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier of G:] is non empty set

the of c

[: the carrier' of c

bool [: the carrier' of c

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

[: the carrier' of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier' of G, the carrier of G:] is non empty set

the of c

[: the carrier' of c

bool [: the carrier' of c

the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of c

bool the carrier' of c

X2 is set

A is Element of the carrier' of G

s1 is Element of the carrier' of c

X2 is set

A is Element of the carrier' of c

s1 is Element of the carrier' of G

X is non empty set

(X) is non empty non void V67() () ()

the carrier' of (X) is non empty set

X * is functional non empty FinSequence-membered M16(X)

X is non empty set

(X) is non empty non void V67() () ()

the carrier' of (X) is functional non empty set

X * is functional non empty FinSequence-membered M16(X)

G is Relation-like Function-like Element of the carrier' of (X)

X is non empty set

(X) is non empty non void V67() () ()

the carrier' of (X) is functional non empty set

[:NAT, the carrier' of (X):] is Relation-like non empty V46() set

bool [:NAT, the carrier' of (X):] is non empty V46() set

c

X * is functional non empty FinSequence-membered M16(X)

c

X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

len X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

s1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

c

A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

s1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

e1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

s2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

c

len e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

e2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)

((X),e2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)

the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]

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

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

the of (X) . e2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)

q2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

len q2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

s2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

c

(X,1,e1) is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

dom e1 is Element of bool NAT

s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

c

len s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

c

len s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

s2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)

the carrier' of (X) is functional non empty set

c

((X),c

the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]

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

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

the of (X) . c

((X),c

the carrier of (X) is non empty set

the of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]

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

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

the of (X) . c

((X),((X),c

the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]

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

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

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

the of (X) . (((X),c

[((X),c

{((X),c

{((X),c

{{((X),c

the of (X) . [((X),c

X * is functional non empty FinSequence-membered M16(X)

X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

X2 . 1 is set

<*(X2 . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like set

[1,(X2 . 1)] is set

{1,(X2 . 1)} is non empty set

{1} is non empty trivial V53(1) set

{{1,(X2 . 1)},{1}} is non empty set

{[1,(X2 . 1)]} is Relation-like Function-like constant non empty trivial V53(1) set

(X,1,X2) is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

<*(X2 . 1)*> ^ (X,1,X2) is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set

dom X2 is Element of bool NAT

A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)

s1 is Element of the carrier of (X)

((X),A,s1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)

the of (X) . (s1,A) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)

[s1,A] is set

{s1,A} is non empty set

{s1} is non empty trivial V53(1) set

{{s1,A},{s1}} is non empty set

the of (X) . [s1,A] is Relation-like Function-like set

((X),A,((X),c

the of (X) . (((X),c

[((X),c

{((X),c

{{((X),c

the of (X) . [((X),c

the carrier' of (X) is functional non empty set

the carrier of (X) is non empty set

c

X2 is Element of the carrier of (X)

((X),c

the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]

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

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

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

the of (X) . (X2,c

[X2,c

{X2,c

{X2} is non empty trivial V53(1) set

{{X2,c

the of (X) . [X2,c

((X),((X),c

the of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]

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

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

the of (X) . ((X),c

X * is functional non empty FinSequence-membered M16(X)

s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

<*X2*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)

[1,X2] is set

{1,X2} is non empty set

{1} is non empty trivial V53(1) set

{{1,X2},{1}} is non empty set

{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set

A is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

<*X2*> ^ A is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set

s1 . 1 is set

the carrier' of (X) is functional non empty set

the carrier of (X) is non empty set

c

X2 is Element of the carrier of (X)

((X),c

the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]

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

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

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

the of (X) . (X2,c

[X2,c

{X2,c

{X2} is non empty trivial V53(1) set

{{X2,c

the of (X) . [X2,c

((X),((X),c

the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]

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

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

the of (X) . ((X),c

X * is functional non empty FinSequence-membered M16(X)

s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

<*X2*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)

[1,X2] is set

{1,X2} is non empty set

{1} is non empty trivial V53(1) set

{{1,X2},{1}} is non empty set

{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set

A is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

<*X2*> ^ A is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set

Del ((<*X2*> ^ A),1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set

the carrier' of (X) is functional non empty set

the carrier of (X) is non empty set

c

X2 is Element of the carrier of (X)

((X),c

the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]

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

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

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

the of (X) . (X2,c

[X2,c

{X2,c

{X2} is non empty trivial V53(1) set

{{X2,c

the of (X) . [X2,c

X * is functional non empty FinSequence-membered M16(X)

<*X2*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)

[1,X2] is set

{1,X2} is non empty set

{1} is non empty trivial V53(1) set

{{1,X2},{1}} is non empty set

{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set

A is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *

<*X2*> ^ A is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set

the non empty set is non empty set

( the non empty set ) is non empty non void V67() () () () () () () ()

X is non empty non void V67() ()

the carrier' of X is non empty set

the Element of the carrier' of X is Element of the carrier' of X

X2 is Element of the carrier' of X

(X,X2) is Element of the carrier' of X

the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]

[: the carrier' of X, the carrier' of X:] is Relation-like non empty set

bool [: the carrier' of X, the carrier' of X:] is non empty set

the of X . X2 is Element of the carrier' of X

[:NAT, the carrier' of X:] is Relation-like non empty V46() set

bool [:NAT, the carrier' of X:] is non empty V46() set

c

c

X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

c

A is Element of the carrier' of X

X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

c

(X,A) is Element of the carrier' of X

the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]

[: the carrier' of X, the carrier' of X:] is Relation-like non empty set

bool [: the carrier' of X, the carrier' of X:] is non empty set

the of X . A is Element of the carrier' of X

X is non empty non void V67() () ()

the of X is Element of bool the carrier' of X

the carrier' of X is non empty set

bool the carrier' of X is non empty set

G is Element of the carrier' of X

X is non empty non void V67() ()

the carrier' of X is non empty set

the carrier of X is non empty set

G is Element of the carrier' of X

c

X2 is Element of the carrier of X

(X,G,X2) is Element of the carrier' of X

the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]

[: the carrier of X, the carrier' of X:] is Relation-like non empty set

[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set

bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set

the of X . (X2,G) is Element of the carrier' of X

[X2,G] is set

{X2,G} is non empty set

{X2} is non empty trivial V53(1) set

{{X2,G},{X2}} is non empty set

the of X . [X2,G] is set

A is Element of the carrier of X

(X,c

the of X . (A,c

[A,c

{A,c

{A} is non empty trivial V53(1) set

{{A,c

the of X . [A,c

(X,(X,G,X2)) is Element of the carrier of X

the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]

[: the carrier' of X, the carrier of X:] is Relation-like non empty set

bool [: the carrier' of X, the carrier of X:] is non empty set

the of X . (X,G,X2) is Element of the carrier of X

(X,(X,c

the of X . (X,c

(X,(X,G,X2)) is Element of the carrier' of X

the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]

[: the carrier' of X, the carrier' of X:] is Relation-like non empty set

bool [: the carrier' of X, the carrier' of X:] is non empty set

the of X . (X,G,X2) is Element of the carrier' of X

(X,(X,c

the of X . (X,c

X is non empty non void V67() ()

the carrier' of X is non empty set

G is Element of the carrier' of X

(X,G) is Element of the carrier' of X

the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]

[: the carrier' of X, the carrier' of X:] is Relation-like non empty set

bool [: the carrier' of X, the carrier' of X:] is non empty set

the of X . G is Element of the carrier' of X

(X,G) is Element of the carrier of X

the carrier of X is non empty set

the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]

[: the carrier' of X, the carrier of X:] is Relation-like non empty set

bool [: the carrier' of X, the carrier of X:] is non empty set

the of X . G is Element of the carrier of X

c

(X,c

the of X . c

(X,c

the of X . c

(X,(X,G),(X,G)) is Element of the carrier' of X

the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]

[: the carrier of X, the carrier' of X:] is Relation-like non empty set

[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set

bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set

the of X . ((X,G),(X,G)) is Element of the carrier' of X

[(X,G),(X,G)] is set

{(X,G),(X,G)} is non empty set

{(X,G)} is non empty trivial V53(1) set

{{(X,G),(X,G)},{(X,G)}} is non empty set

the of X . [(X,G),(X,G)] is set

F

the carrier' of F

the carrier of F

F

G is Element of the carrier' of F

(F

the of F

[: the carrier' of F

bool [: the carrier' of F

the of F

[:NAT, the carrier' of F

bool [:NAT, the carrier' of F

X is Relation-like NAT -defined the carrier' of F

X . 0 is Element of the carrier' of F

G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

X . G is Element of the carrier' of F

c

G + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X . (G + 1) is Element of the carrier' of F

(F

the of F

[: the carrier' of F

bool [: the carrier' of F

the of F

G -' 0 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X . (G -' 0) is Element of the carrier' of F

X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set

G -' X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X . (G -' X2) is Element of the carrier' of F

X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

G -' (X2 + 1) is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

(G -' X2) -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

(G -' (X2 + 1)) + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X . (G -' (X2 + 1)) is Element of the carrier' of F

(F

the of F

(F

the of F

[: the carrier' of F

bool [: the carrier' of F

the of F

(F

the of F

[: the carrier of F

[:[: the carrier of F

bool [:[: the carrier of F

the of F

[(F

{(F

{(F

{{(F

the of F

0 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

0 -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X . (G -' (X2 + 1)) is Element of the carrier' of F

0 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

G -' G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT

X . (G -' G) is Element of the carrier' of F

F

the carrier' of F

F

[: the carrier' of F

bool [: the carrier' of F

F

F

the carrier of F

bool [: the carrier' of F

bool (bool [: the carrier' of F

X is set

G is Element of the carrier' of F

[G,F

{G,F

{G} is non empty trivial V53(1) set

{{G,F

c

A is Element of F

[c

{c

{c

{{c

X2 is Element of the carrier of F

(F

the of F

[: the carrier of F

[:[: the carrier of F

bool [:[: the carrier of F

the of F

[X2,c

{X2,c

{X2} is non empty trivial V53(1) set

{{X2,c

the of F

F

[(F

{(F

{(F

{{(F

G is non empty set

meet G is set

X2 is Relation-like the carrier' of F

A is Element of the carrier' of F

[A,F

{A,F

{A} is non empty trivial V53(1) set

{{A,F

s1 is set

A is Element of the carrier' of F

s1 is Element of the carrier of F

(F

the of F

[: the carrier of F

[:[: the carrier of F

bool [:[: the carrier of F

the of F

[s1,A] is set

{s1,A} is non empty set

{s1} is non empty trivial V53(1) set

{{s1,A},{s1}} is non empty set

the of F

s2 is Element of F

[A,s2] is Element of [: the carrier' of F

{A,s2} is non empty set

{A} is non empty trivial V53(1) set

{{A,s2},{A}} is non empty set

F

[(F

{(F

{(F

{{(F

e1 is set

e2 is Element of the carrier' of F

[e2,F

{e2,F

{e2} is non empty trivial V53(1) set

{{e2,F

q2 is Element of the carrier' of F

e2 is Element of F

[q2,e2] is Element of [: the carrier' of F

{q2,e2} is non empty set

{q2} is non empty trivial V53(1) set

{{q2,e2},{q2}} is non empty set

e1 is Element of the carrier of F

(F

the of F

[e1,q2] is set

{e1,q2} is non empty set

{e1} is non empty trivial V53(1) set

{{e1,q2},{e1}} is non empty set

the of F

F

[(F

{(F

{(F

{{(F

A is Element of the carrier' of F

s1 is Element of F

[A,s1] is set

{A,s1} is non empty set

{A} is non empty trivial V53(1) set

{{A,s1},{A}} is non empty set

[A,F

{A,F

{{A,F

s2 is set

A is Element of the carrier' of F

s1 is Element of the carrier of F

(F

the of F

[: the carrier of F

[:[: the carrier of F

bool [:[: the carrier of F

the of F

[s1,A] is set

{s1,A} is non empty set

{s1} is non empty trivial V53(1) set

{{s1,A},{s1}} is non empty set

the of F

s2 is set

[A,s2] is set

{A,s2} is non empty set

{A} is non empty trivial V53(1) set

{{A,s2