:: FOMODEL0 semantic presentation

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

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

bool omega is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered set
RAT is non empty non trivial non finite non empty-membered set
INT is non empty non trivial non finite non empty-membered set
is Relation-like non empty non trivial non finite non empty-membered set
bool is non empty non trivial non finite non empty-membered set
K281() is non empty strict multMagma
the U1 of K281() is set

K391(NAT) is V165() set

omega \/ is non empty set
is non empty V15() set

() \ is Element of bool ()
bool () is non empty set
Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT
{ } is set

K587() is set
K588() is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
U is set

[:U,U:] is Relation-like set
[:[:U,U:],U:] is Relation-like set
bool [:[:U,U:],U:] is non empty set
U is set

U is set
union U is set
q1 is set
q2 is set
Funcs (q1,q2) is functional set
[:q1,q2:] is Relation-like set
bool [:q1,q2:] is non empty Element of bool (bool [:q1,q2:])
bool [:q1,q2:] is non empty set
bool (bool [:q1,q2:]) is non empty set
bool (bool [:q1,q2:]) is non empty set
p is Element of bool (bool [:q1,q2:])
union p is Relation-like q1 -defined q2 -valued Element of bool [:q1,q2:]
U is set

proj1 q1 is set
(proj1 q1) /\ U is set

f is set
q11 is set
q1 . f is set
q1 . q11 is set
proj1 (q1 | U) is set
(q1 | U) . f is set
(q1 | U) . q11 is set
f is set
proj1 (q1 | U) is set
q11 is set
(q1 | U) . f is set
(q1 | U) . q11 is set
q1 . f is set
q1 . q11 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is set
q2 is set

(f | q2) | q1 is Relation-like [:U,U:] -defined q1 -defined [:U,U:] -defined U -valued Function-like Element of bool [:[:U,U:],U:]
U is set
q1 is set

(q2 -tuples_on U) /\ (f -tuples_on q1) is set
q11 is set

{ } is set
q1 is set

Funcs ((Seg U),q1) is functional set
q2 is non empty set

Funcs ((Seg U),q2) is functional non empty FUNCTION_DOMAIN of Seg U,q2
U is set
q1 is set

(q2 -tuples_on U) /\ (q1 *) is set

p is set

{ } is set

bool q1 is non empty set
Funcs ((Seg q2),q1) is functional set
U is set
q1 is set

(q2 -tuples_on U) /\ (q1 *) is set

(q2 -tuples_on U) /\ (q2 -tuples_on q1) is set
(q2 -tuples_on U) /\ ((q2 -tuples_on U) /\ (q1 *)) is set
(q2 -tuples_on U) /\ (q2 -tuples_on U) is set
((q2 -tuples_on U) /\ (q2 -tuples_on U)) /\ (q1 *) is set
p is set

U is set
q1 is set
Funcs (U,q1) is functional set
q2 is set
Funcs (U,q2) is functional set
(Funcs (U,q1)) /\ (Funcs (U,q2)) is set
q1 /\ q2 is set
Funcs (U,(q1 /\ q2)) is functional set
F is set

proj1 p is set
proj2 p is set

proj1 C is set
proj2 C is set
U is set
q1 is set

U /\ q1 is set

(q2 -tuples_on U) /\ (q1 *) is set
q2 -tuples_on (U /\ q1) is functional FinSequence-membered FinSequenceSet of U /\ q1

{ } is set
Funcs ((Seg q2),(U /\ q1)) is functional set
Funcs ((Seg q2),U) is functional set
Funcs ((Seg q2),q1) is functional set
(Funcs ((Seg q2),U)) /\ (Funcs ((Seg q2),q1)) is set
(q2 -tuples_on U) /\ (Funcs ((Seg q2),q1)) is set

(q2 -tuples_on U) /\ (q2 -tuples_on q1) is set
U is set
q1 is set
U /\ q1 is set

q2 -tuples_on (U /\ q1) is functional FinSequence-membered FinSequenceSet of U /\ q1

(q2 -tuples_on U) /\ (q2 -tuples_on q1) is set

(q2 -tuples_on U) /\ (q1 *) is set
U is non empty set
U -concatenation is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]

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

() . (q1,q2) is set
[q1,q2] is non empty V15() set

the U1 of (U *+^) is set

the multF of (U *+^) is Relation-like [: the U1 of (U *+^), the U1 of (U *+^):] -defined the U1 of (U *+^) -valued Function-like quasi_total Element of bool [:[: the U1 of (U *+^), the U1 of (U *+^):], the U1 of (U *+^):]
[: the U1 of (U *+^), the U1 of (U *+^):] is Relation-like set
[:[: the U1 of (U *+^), the U1 of (U *+^):], the U1 of (U *+^):] is Relation-like set
bool [:[: the U1 of (U *+^), the U1 of (U *+^):], the U1 of (U *+^):] is non empty set

() . (F,p) is set
[F,p] is non empty V15() set

U is non empty set
U -concatenation is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]

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

() . (q1,q2) is set
[q1,q2] is non empty V15() set

() . (q11,F) is set
[q11,F] is non empty V15() set

U is non empty set

(U *) \ is functional FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
q1 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is set
q2 is set

[:q1,U:] is Relation-like set
[:q2,U:] is Relation-like set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

proj1 <:U,q1:> is set

Seg (min ((len U),(len q1))) is finite min ((len U),(len q1)) -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= min ((len U),(len q1)) ) } is set

(dom U) /\ (dom q1) is finite countable Element of bool NAT

{ } is set
(Seg (len U)) /\ (dom q1) is finite countable Element of bool NAT

{ } is set
(Seg (len U)) /\ (Seg (len q1)) is finite countable Element of bool NAT
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

pr1 (U,U) is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
q1 is Element of U
q2 is Element of U
f is Element of U
(U) . (q2,f) is Element of U
[q2,f] is non empty V15() set
(U) . [q2,f] is set
(U) . (q1,((U) . (q2,f))) is Element of U
[q1,((U) . (q2,f))] is non empty V15() set
(U) . [q1,((U) . (q2,f))] is set
(U) . (q1,q2) is Element of U
[q1,q2] is non empty V15() set
(U) . [q1,q2] is set
(U) . (((U) . (q1,q2)),f) is Element of U
[((U) . (q1,q2)),f] is non empty V15() set
(U) . [((U) . (q1,q2)),f] is set
(U) . (q1,f) is Element of U
[q1,f] is non empty V15() set
(U) . [q1,f] is set

U is set
[:U,U:] is Relation-like set
[:[:U,U:],U:] is Relation-like set
bool [:[:U,U:],U:] is non empty set
q1 is non empty set
(q1) is Relation-like [:q1,q1:] -defined q1 -valued Function-like non empty total quasi_total associative Element of bool [:[:q1,q1:],q1:]
[:q1,q1:] is Relation-like non empty set
[:[:q1,q1:],q1:] is Relation-like non empty set
bool [:[:q1,q1:],q1:] is non empty set
pr1 (q1,q1) is Relation-like [:q1,q1:] -defined q1 -valued Function-like non empty total quasi_total Element of bool [:[:q1,q1:],q1:]

bool [:[:q1,q1:],q1:] is non empty finite finite-membered countable set
U is set
bool U is non empty set
q1 is Element of bool U

bool (U *) is non empty set
U is non empty set

[:(U *),(U *):] is Relation-like non empty set
[:[:(U *),(U *):],(U *):] is Relation-like non empty set
bool [:[:(U *),(U *):],(U *):] is non empty set
U -concatenation is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]
q1 is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]
U is non empty set

(U *) \ is functional FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
the Element of U is Element of U

[1, the Element of U] is non empty V15() set

U is non empty set

U is set

proj1 q1 is set
U /\ (proj1 q1) is set
q2 is set
f is set
q1 . q2 is set
q1 . f is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

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

proj1 U is set
U . q1 is set

{q1} --> (U . q1) is Relation-like {q1} -defined {(U . q1)} -valued Function-like constant non empty total quasi_total finite countable finite-support Element of bool [:{q1},{(U . q1)}:]
{(U . q1)} is non empty trivial finite 1 -element countable set
[:{q1},{(U . q1)}:] is Relation-like non empty finite countable set
bool [:{q1},{(U . q1)}:] is non empty finite finite-membered countable set
proj1 U is set

proj1 U is set

U is set

q1 is non empty set

U is non empty set

bool U is non empty set
q1 is Element of bool U
q2 is non empty set

U is set

q2 is set

U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

U is non empty set

[:(U *),(U *):] is Relation-like non empty set
[:[:(U *),(U *):],(U *):] is Relation-like non empty set
bool [:[:(U *),(U *):],(U *):] is non empty set
q1 /\ () is Relation-like NAT -defined [:(U *),(U *):] -defined U * -valued finite countable (U * ,U -concatenation ) Element of bool [:[:(U *),(U *):],(U *):]
U is non empty set

U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

q2 . 1 is set

proj1 f is set
f . {} is set

f . (q11 + 1) is set
f . q11 is set

q2 . (q11 + 2) is set
q1 . ((f . q11),(q2 . (q11 + 2))) is set
[(f . q11),(q2 . (q11 + 2))] is non empty V15() set
q1 . [(f . q11),(q2 . (q11 + 2))] is set

proj1 f is set
f . {} is set

proj1 q11 is set
q11 . {} is set

f . (F + 1) is set
f . F is set

q2 . (F + 2) is set
q1 . ((f . F),(q2 . (F + 2))) is set
[(f . F),(q2 . (F + 2))] is non empty V15() set
q1 . [(f . F),(q2 . (F + 2))] is set

q11 . (F + 1) is set
q11 . F is set

q2 . (F + 2) is set
q1 . ((q11 . F),(q2 . (F + 2))) is set
[(q11 . F),(q2 . (F + 2))] is non empty V15() set
q1 . [(q11 . F),(q2 . (F + 2))] is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

(U,q1,q2) is Relation-like Function-like set

(U,q1,q2) . {} is set

{ } is set

q2 . 1 is set

bool U is non empty set

(U,q1,q2) . f is set

(U,q1,q2) . (f + 1) is set

{ } is set

q2 . (f + 2) is set

bool U is non empty set
[((U,q1,q2) . f),(q2 . (f + 2))] is non empty V15() set
q1 . (((U,q1,q2) . f),(q2 . (f + 2))) is set
q1 . [((U,q1,q2) . f),(q2 . (f + 2))] is set

{ } is set

(U,q1,(q2 | f)) is Relation-like Function-like set
(U,q1,(q2 | f)) . {} is set
(q2 | f) . 1 is set
q2 . 1 is set

(U,q1,q2) . f is set

(U,q1,q2) . (f + 1) is set

Seg q11 is finite q11 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q11 ) } is set

(U,q1,(q2 | q11)) is Relation-like Function-like set
(U,q1,(q2 | q11)) . (f + 1) is set

(U,q1,(q2 | q11)) . f is set
(q2 | q11) . (f + 2) is set
q1 . (((U,q1,(q2 | q11)) . f),((q2 | q11) . (f + 2))) is set
[((U,q1,(q2 | q11)) . f),((q2 | q11) . (f + 2))] is non empty V15() set
q1 . [((U,q1,(q2 | q11)) . f),((q2 | q11) . (f + 2))] is set
q1 . (((U,q1,q2) . f),((q2 | q11) . (f + 2))) is set
[((U,q1,q2) . f),((q2 | q11) . (f + 2))] is non empty V15() set
q1 . [((U,q1,q2) . f),((q2 | q11) . (f + 2))] is set
q2 . (f + 2) is set
q1 . (((U,q1,q2) . f),(q2 . (f + 2))) is set
[((U,q1,q2) . f),(q2 . (f + 2))] is non empty V15() set
q1 . [((U,q1,q2) . f),(q2 . (f + 2))] is set

{ } is set

(U,q1,(q2 | f)) is Relation-like Function-like set
(U,q1,(q2 | f)) . {} is set

(U,q1,q2) . f is set

Seg q11 is finite q11 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q11 ) } is set

(U,q1,(q2 | q11)) is Relation-like Function-like set
(U,q1,(q2 | q11)) . (f + 1) is set
(U,q1,q2) . (f + 1) is set

(U,q1,q2) . f is set

{ } is set

(U,q1,(q2 | F)) is Relation-like Function-like set
(U,q1,(q2 | F)) . q11 is set
(U,q1,q2) . q11 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

(U *) \ is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set

(U,q1,q2) is Relation-like Function-like set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

(U *) \ is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
[:((U *) \ ),U:] is Relation-like non empty set
bool [:((U *) \ ),U:] is non empty set

(U,q1,q2) is Relation-like Function-like set
(U,q1,q2) is Relation-like Function-like set

(U,q1,q2) . ((len q2) - 1) is set

(U,q1,f) is Relation-like Function-like set
(U,q1,f) . q11 is set
F is Element of U
q2 is Relation-like (U *) \ -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ ),U:]

q2 . f is Element of U
(U,q1,f) is Relation-like Function-like set
(U,q1,f) is Relation-like Function-like set

(U,q1,f) . ((len f) - 1) is set
q2 is Relation-like (U *) \ -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ ),U:]
f is Relation-like (U *) \ -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ ),U:]
dom q2 is functional non empty FinSequence-membered Element of bool ((U *) \ )
bool ((U *) \ ) is non empty set
dom f is functional non empty FinSequence-membered Element of bool ((U *) \ )
q11 is set
q2 . q11 is set

(U,q1,F) is Relation-like Function-like set
(U,q1,F) is Relation-like Function-like set

(U,q1,F) . ((len F) - 1) is set
f . q11 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

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

(U *) \ is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
[:((U *) \ ),U:] is Relation-like non empty set
bool [:((U *) \ ),U:] is non empty set

(U,q1) . f is set
q11 is Element of U

[1,q11] is non empty V15() set

(U,q1) . <*q11*> is set

(U,q1) . (f ^ <*q11*>) is set
q1 . (((U,q1) . f),q11) is set
[((U,q1) . f),q11] is non empty V15() set
q1 . [((U,q1) . f),q11] is set

dom <*q11*> is non empty trivial finite 1 -element countable Element of bool NAT

C . ((len f) + 1) is set
<*q11*> . 1 is set

Seg (len f) is non empty finite len f -element countable Element of bool NAT
{ } is set

(U,q1) . x is Element of U
(U,q1,x) is Relation-like Function-like set
(U,q1,x) is Relation-like Function-like set
(U,q1,x) . {} is set
x . 1 is set

(U,q1) . y is Element of U
(U,q1,y) is Relation-like Function-like set
(U,q1,y) is Relation-like Function-like set

(U,q1,y) . ((len y) - 1) is set
(U,q1,y) . F is set

y . (F + 2) is set
q1 . (((U,q1,y) . F),(y . (F + 2))) is set
[((U,q1,y) . F),(y . (F + 2))] is non empty V15() set
q1 . [((U,q1,y) . F),(y . (F + 2))] is set

(U,q1,p) is Relation-like Function-like set
(U,q1,p) is Relation-like Function-like set

(U,q1,p) . ((len f) - 1) is set
y . ((len f) + 1) is set
q1 . (((U,q1,p) . ((len f) - 1)),(y . ((len f) + 1))) is set
[((U,q1,p) . ((len f) - 1)),(y . ((len f) + 1))] is non empty V15() set
q1 . [((U,q1,p) . ((len f) - 1)),(y . ((len f) + 1))] is set
(U,q1) . p is Element of U
q1 . (((U,q1) . p),q11) is Element of U
[((U,q1) . p),q11] is non empty V15() set
q1 . [((U,q1) . p),q11] is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

dom q1 is Relation-like U -defined U -valued non empty Element of bool [:U,U:]
bool [:U,U:] is non empty set
q2 is set
[:q2,U:] is Relation-like set
q2 /\ U is set
f is set
q11 is set
F is set
p is set
q1 . (f,F) is set
[f,F] is non empty V15() set
q1 . [f,F] is set
q1 . (q11,p) is set
[q11,p] is non empty V15() set
q1 . [q11,p] is set
U /\ U is set
[:(q2 /\ U),(U /\ U):] is Relation-like set
[:q2,U:] /\ [:U,U:] is Relation-like set
f is set
[:q2,U:] /\ (dom q1) is Relation-like U -defined U -valued Element of bool [:U,U:]
q11 is set
q1 . f is set
q1 . q11 is set
U /\ U is set
[:(q2 /\ U),(U /\ U):] is Relation-like set
F is set
p is set
[F,p] is non empty V15() set
C is set
y1 is set
[C,y1] is non empty V15() set
q1 . (F,p) is set
q1 . [F,p] is set
q1 . (C,y1) is set
q1 . [C,y1] is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

q2 is set
q2 /\ U is set
[:q2,U:] is Relation-like set
f is set
q11 is set
F is set
p is set
q1 . (f,F) is set
[f,F] is non empty V15() set
q1 . [f,F] is set
q1 . (q11,p) is set
[q11,p] is non empty V15() set
q1 . [q11,p] is set
[:q2,U:] is Relation-like set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set

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

(U *) \ is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
[:((U *) \ ),U:] is Relation-like non empty set
bool [:((U *) \ ),U:] is non empty set
f is Element of U

[1,f] is non empty V15() set

(U,q1) . (<*f*> ^ q11) is set
(U,q1) . q11 is set
q1 . (f,((U,q1) . q11)) is set
[f,((U,q1) . q11)] is non empty V15() set
q1 . [f,((U,q1) . q11)] is set
F is Element of U

[1,F] is non empty V15() set

(U,q1) . <*f*> is set
q1 . (((U,q1) . <*f*>),F) is set
[((U,q1) . <*f*>),F] is non empty V15() set
q1 . [((U,q1) . <*f*>),F] is set
q1 . (f,F) is Element of U
[f,F] is non empty V15() set
q1 . [f,F] is set

((q11 + 1) + 1) -tuples_on U is functional non empty FinSequence-membered with_non-empty_elements non empty-membered FinSequenceSet of U

(U,q1) . (<*f*> ^ F) is set
(U,q1) . F is set
q1 . (f,((U,q1) . F)) is set
[f,((U,q1) . F)] is non empty V15() set
q1 . [f,((U,q1) . F)] is set

Seg (q11 + 1) is non empty finite q11 + 1 -element q11 + 1 -element countable Element of bool NAT

{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q11 + 1 ) } is set

F /. (len F) is Element of U

(U,q1) . C is set
y1 is Element of U

[1,y1] is non empty V15() set

(U,q1) . (<*f*> ^ ((F | (q11 + 1)) ^ <*y1*>)) is set

(U,q1) . ((<*f*> ^ p) ^ <*y1*>) is set
(U,q1) . (<*f*> ^ p) is set
q1 . (((U,q1) . (<*f*> ^ p)),y1) is set
[((U,q1) . (<*f*> ^ p)),y1] is non empty V15() set
q1 . [((U,q1) . (<*f*> ^ p)),y1] is set
(U,q1) . p is set
q1 . (f,((U,q1) . p)) is set
[f,((U,q1) . p)] is non empty V15() set
q1 . [f,((U,q1) . p)] is set
q1 . ((q1 . (f,((U,q1) . p))),y1) is set
[(q1 . (f,((U,q1) . p))),y1] is non empty V15() set
q1 . [(q1 . (f,((U,q1) . p))),y1] is set
x is Element of U
q1 . (x,y1) is Element of U
[x,y1] is non empty V15() set
q1 . [x,y1] is set
q1 . (f,(q1 . (x,y1))) is Element of U
[f,(q1 . (x,y1))] is non empty V15() set
q1 . [f,(q1 . (x,y1))] is set

(U,q1) . (C ^