:: FACIRC_1 semantic presentation

REAL is set
NAT is non empty V5() V7() V8() V9() non finite V44() V45() countable denumerable Element of K19(REAL)
K19(REAL) is set

RAT is set
INT is set

K19(K20(COMPLEX,COMPLEX)) is set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is Relation-like set
K19(K20(K20(REAL,REAL),REAL)) is set

K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is Relation-like set
K19(K20(K20(RAT,RAT),RAT)) is set

K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is Relation-like set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5() Relation-like non finite set
K20(K20(NAT,NAT),NAT) is V5() Relation-like non finite set
K19(K20(K20(NAT,NAT),NAT)) is V5() non finite set
NAT is non empty V5() V7() V8() V9() non finite V44() V45() countable denumerable set
K19(NAT) is V5() non finite set
K19(NAT) is V5() non finite set
BOOLEAN is non empty set

1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() finite V44() countable Element of NAT
{0,1} is non empty finite V43() countable set
{{},1} is non empty finite V43() countable set
K363() is set
K19(K363()) is set
K364() is Element of K19(K363())
K404() is non empty V98() L10()
the carrier of K404() is non empty set
K367( the carrier of K404()) is non empty M24( the carrier of K404())
K403(K404()) is Element of K19(K367( the carrier of K404()))
K19(K367( the carrier of K404())) is set
K20(K403(K404()),NAT) is Relation-like set
K19(K20(K403(K404()),NAT)) is set
K20(NAT,K403(K404())) is Relation-like set
K19(K20(NAT,K403(K404()))) is set
2 is V1() V2() V3() non empty V7() V8() V9() V13() V14() finite V44() countable Element of NAT
3 is V1() V2() V3() non empty V7() V8() V9() V13() V14() finite V44() countable Element of NAT
x is set
y is set
c is set
[y,c] is pair set
{y,c} is non empty finite countable set
{y} is non empty V5() finite V46(1) countable set
{{y,c},{y}} is non empty finite V43() countable set
x is set
y is set
[x,y] is non empty pair set
{x,y} is non empty finite countable set
{x} is non empty V5() finite V46(1) countable set
{{x,y},{x}} is non empty finite V43() countable set
x is V1() V3() V7() V8() V9() V13() V14() finite V44() countable set
y is set
c is set
[y,c] is non empty pair set
{y,c} is non empty finite countable set
{y} is non empty V5() finite V46(1) countable set
{{y,c},{y}} is non empty finite V43() countable set
{ b1 where b1 is V1() V3() V7() V8() V9() V13() V14() finite V44() countable Element of NAT : b1 < x } is set
x is set
y is non empty pair set
x is non pair set
{x} is non empty V5() finite V46(1) countable set
y is non empty pair set
y is non pair set
{x,y} is non empty finite countable set
c is non empty pair set
c is non pair set
{x,y,c} is finite countable set
S1 is non empty pair set
the non pair set is non pair set
{ the non pair set } is non empty V5() finite V46(1) countable () set
x is () set
y is () set
x \/ y is set
c is non empty pair set
x is () set
y is set
x \ y is Element of K19(x)
K19(x) is set
c is non empty pair set
x /\ y is set
c is non empty pair set
y /\ x is () set
x is non empty pair set
{x} is non empty V5() finite V46(1) countable set
y is set
y is non empty pair set
{x,y} is non empty finite countable set
c is set
c is non empty pair set
{x,y,c} is finite countable set
S1 is set
x is set
y is non empty set
the Element of y is Element of y
S1 is set
S2 is set
[S1,S2] is non empty pair set
{S1,S2} is non empty finite countable set
{S1} is non empty V5() finite V46(1) countable set
{{S1,S2},{S1}} is non empty finite V43() countable set
x is non pair set

y is set
proj1 <*x*> is non empty V5() finite V46(1) countable set
<*x*> . y is set
dom <*x*> is non empty V5() finite V46(1) countable Element of K19(NAT)
proj2 <*x*> is non empty V5() finite V46(1) countable set
{x} is non empty V5() finite V46(1) countable () set
y is non pair set

c is set
proj1 <*x,y*> is non empty finite V46(2) countable set
<*x,y*> . c is set
dom <*x,y*> is non empty finite V46(2) countable Element of K19(NAT)
proj2 <*x,y*> is non empty finite countable set
{x,y} is non empty finite countable () set
c is non pair set

S1 is set
proj1 <*x,y,c*> is non empty finite V46(3) countable set
<*x,y,c*> . S1 is set
dom <*x,y,c*> is non empty finite V46(3) countable Element of K19(NAT)
proj2 <*x,y,c*> is non empty finite countable set
{x,y,c} is finite countable () set

proj2 x is set
proj1 x is set
y is non empty pair set
c is set
x . c is set
x is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
Seg x is finite V46(x) countable Element of K19(NAT)

K20((Seg x),(Seg x)) is Relation-like finite countable set
K19(K20((Seg x),(Seg x))) is finite V43() countable set

len y is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT

len () is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT

S1 is set

c . S1 is set
dom c is finite V46(x) countable Element of K19(NAT)
the V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set

proj2 x is set
x is non empty V74() ManySortedSign
y is non empty V74() ManySortedSign
InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty V74() strict ManySortedSign
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))

S1 is Relation-like set
c \/ S1 is Relation-like set

InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)

InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)

InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
x is non empty V74() ManySortedSign
y is non empty V74() ManySortedSign
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
x +* y is non empty V74() strict ManySortedSign
InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
InputVertices y is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InnerVertices x is Element of K19( the carrier of x)
() \ () is Element of K19( the carrier of y)
() \/ (() \ ()) is set
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
proj2 the ResultSort of (x +* y) is set
proj2 the ResultSort of x is set
proj2 the ResultSort of y is set
(proj2 the ResultSort of x) \/ (proj2 the ResultSort of y) is set
the carrier of x \/ the carrier of y is non empty set
A1 is set
() \/ () is set
A1 is set
A1 is set
() \ (proj2 the ResultSort of x) is Element of K19( the carrier of y)
x is set
y is set
c is set
S1 is set
S2 is set
[S1,S2] is non empty pair set
{S1,S2} is non empty finite countable set
{S1} is non empty V5() finite V46(1) countable set
{{S1,S2},{S1}} is non empty finite V43() countable set

InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)

InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)

InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
InputVertices y is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InnerVertices x is Element of K19( the carrier of x)
() \ () is Element of K19( the carrier of y)
() \/ (() \ ()) is set

InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InnerVertices x is Element of K19( the carrier of x)

InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InnerVertices y is Element of K19( the carrier of y)

InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
() \/ () is set
() \ () is Element of K19( the carrier of y)
() \/ (() \ ()) is set
x is non empty V74() ManySortedSign
y is non empty V74() ManySortedSign
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty V74() strict ManySortedSign
InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
() \/ () is set
c is non empty pair set

InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)

InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)

InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

S1 is boolean Element of BOOLEAN

y . <*c,S1*> is boolean set

S2 . 1 is set
S2 . 2 is set
F1((S2 . 1),(S2 . 2)) is boolean Element of BOOLEAN
F1(c,(S2 . 2)) is boolean Element of BOOLEAN
F1(c,S1) is boolean Element of BOOLEAN

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN

x . c is boolean Element of BOOLEAN
F1(S1,S2) is boolean Element of BOOLEAN
y . c is boolean Element of BOOLEAN

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

S1 is boolean Element of BOOLEAN

y . <*c,S1*> is boolean set

S2 . 1 is set
S2 . 2 is set
F1((S2 . 1),(S2 . 2)) is boolean Element of BOOLEAN
F1(c,(S2 . 2)) is boolean Element of BOOLEAN
F1(c,S1) is boolean Element of BOOLEAN

S2 is boolean Element of BOOLEAN

y . S1 is boolean Element of BOOLEAN
F1(S2,A) is boolean Element of BOOLEAN
c . S1 is boolean Element of BOOLEAN

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN

y . <*c,S1,S2*> is boolean set

A . 1 is set
A . 2 is set
A . 3 is set
F1((A . 1),(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,S2) is boolean Element of BOOLEAN

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN

x . c is boolean Element of BOOLEAN
F1(S1,S2,A) is boolean Element of BOOLEAN
y . c is boolean Element of BOOLEAN

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN

y . <*c,S1,S2*> is boolean set

A . 1 is set
A . 2 is set
A . 3 is set
F1((A . 1),(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,S2) is boolean Element of BOOLEAN

S2 is boolean Element of BOOLEAN

A1 is boolean Element of BOOLEAN

y . S1 is boolean Element of BOOLEAN
F1(S2,A,A1) is boolean Element of BOOLEAN
c . S1 is boolean Element of BOOLEAN

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

K20((),BOOLEAN) is Relation-like set
K19(K20((),BOOLEAN)) is set

x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is Element of the carrier' of x
the_result_sort_of S1 is Element of the carrier of x
() . () is set
Den (S1,y) is Relation-like Function-like V29( Args (S1,y), Result (S1,y)) Element of K19(K20((Args (S1,y)),(Result (S1,y))))
Args (S1,y) is non empty Element of proj2 K260( the carrier of x, the Sorts of y)
K260( the carrier of x, the Sorts of y) is Relation-like non-empty the carrier of x * -defined Function-like total set
the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x
proj2 K260( the carrier of x, the Sorts of y) is set
Result (S1,y) is non empty Element of proj2 the Sorts of y
proj2 the Sorts of y is set
K20((Args (S1,y)),(Result (S1,y))) is Relation-like set
K19(K20((Args (S1,y)),(Result (S1,y)))) is set

(Den (S1,y)) . (() * c) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
proj1 the ResultSort of x is set
the ResultSort of x . S1 is Element of the carrier of x
proj2 the ResultSort of x is set
InnerVertices x is non empty Element of K19( the carrier of x)
K19( the carrier of x) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
S1 depends_on_in c is Element of Args (S1,y)
action_at () is Element of the carrier' of x
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

K20(NAT,(product the Sorts of y)) is V5() Relation-like non finite set
K19(K20(NAT,(product the Sorts of y))) is V5() non finite set
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A2 is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
A2 . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A2 . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
s is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
s . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
s . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
s2 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
t is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
t . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
t . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
K20(NAT,(product the Sorts of y)) is V5() Relation-like non finite set
K19(K20(NAT,(product the Sorts of y))) is V5() non finite set
S1 is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
S1 . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
S1 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S1 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
K20(NAT,(product the Sorts of y)) is V5() Relation-like non finite set
K19(K20(NAT,(product the Sorts of y))) is V5() non finite set
S2 is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
S2 . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 . (S1 + 1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
S1 + S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S1 + S2)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S1),S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
S1 + (S2 + 1) is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S1 + (S2 + 1))) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S1),(S2 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 + (S2 + 1) is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S1 + (S2 + 1))) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(S1 + S2) + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,((S1 + S2) + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,(S1 + S2)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 + 0 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S1 + 0)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S1),0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
0 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following () is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
1 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
0 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(0 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,(0 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
S1 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S1 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(),S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,1),S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is set
c . S1 is set
S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,(x,y,c,S2),A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S2),A) . S1 is set
(x,y,c,S2) . S1 is set
S2 + A is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S2 + A)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,(S2 + A)) . S1 is set
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
InputVertices x is Element of K19( the carrier of x)
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is set
c . S1 is set
S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,S2) . S1 is set
S2 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S2 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,(S2 + 1)) . S1 is set
Following (x,y,c,S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(Following (x,y,c,S2)) . S1 is set
(x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,0) . S1 is set
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set

c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is Element of the carrier' of x

the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x

the_result_sort_of S1 is Element of the carrier of x
A is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,(),A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(),A) . () is set
() . () is set
A1 is set
dom () is finite countable Element of K19(NAT)
() . A1 is set
(x,y,c,A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
() * (x,y,c,A) is Relation-like NAT -defined Function-like finite countable set
(() * (x,y,c,A)) . A1 is set
(x,y,c,A) . (() . A1) is set

(() * c) . A1 is set
c . (() . A1) is set
proj1 (x,y,c,A) is set
proj1 (() * (x,y,c,A)) is finite countable set
proj1 c is set
proj1 (() * c) is finite countable set
A + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(A + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,(A + 1)) . () is set
Following (x,y,c,A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(Following (x,y,c,A)) . () is set
Den (S1,y) is Relation-like Function-like V29( Args (S1,y), Result (S1,y)) Element of K19(K20((Args (S1,y)),(Result (S1,y))))
Args (S1,y) is non empty Element of proj2 K260( the carrier of x, the Sorts of y)
K260( the carrier of x, the Sorts of y) is Relation-like non-empty the carrier of x * -defined Function-like total set
proj2 K260( the carrier of x, the Sorts of y) is set
Result (S1,y) is non empty Element of proj2 the Sorts of y
proj2 the Sorts of y is set
K20((Args (S1,y)),(Result (S1,y))) is Relation-like set
K19(K20((Args (S1,y)),(Result (S1,y)))) is set
(Den (S1,y)) . (() * (x,y,c,A)) is set
x is non empty V74() ManySortedSign
the carrier of x is non empty set
y is non empty V74() ManySortedSign
x +* y is non empty V74() strict ManySortedSign
the carrier of (x +* y) is non empty set
y +* x is non empty V74() strict ManySortedSign
the carrier of (y +* x) is non empty set
c is Element of the carrier of x
the carrier of y is non empty set
the carrier of x \/ the carrier of y is non empty set
the carrier of y \/ the carrier of x is non empty set

InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)

InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))

InnerVertices (y +* x) is Element of K19( the carrier of (y +* x))
the carrier of (y +* x) is non empty set
K19( the carrier of (y +* x)) is set
the ResultSort of (y +* x) is Relation-like Function-like V29( the carrier' of (y +* x), the carrier of (y +* x)) Element of K19(K20( the carrier' of (y +* x), the carrier of (y +* x)))
the carrier' of (y +* x) is set
K20( the carrier' of (y +* x), the carrier of (y +* x)) is Relation-like set
K19(K20( the carrier' of (y +* x), the carrier of (y +* x))) is set
K480( the carrier of (y +* x), the ResultSort of (y +* x)) is Element of K19( the carrier of (y +* x))
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
() \/ () is set
() \/ () is set
c is set
y is non empty V74() ManySortedSign
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x is non empty V74() ManySortedSign
x +* y is non empty V74() strict ManySortedSign
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
the carrier of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
the ResultSort of x +* the ResultSort of y is Relation-like Function-like set
proj2 ( the ResultSort of x +* the ResultSort of y) is set
S2 is set

S1 +* S2 is strict non-empty MSAlgebra over x +* y

(S1 +* S2) +* A is strict non-empty MSAlgebra over (x +* y) +* c

S2 +* A is strict non-empty MSAlgebra over y +* c
S1 +* (S2 +* A) is strict non-empty MSAlgebra over x +* (y +* c)

the carrier of c is non empty set

the carrier of x is non empty set

the carrier of y is non empty set

the carrier of (x +* y) is non empty set
the carrier of x is non empty set
the carrier of y is non empty set

the Sorts of (c +* S1) is Relation-like non-empty the carrier of (x +* y) -defined Function-like total set
product the Sorts of (c +* S1) is non empty functional with_common_domain product-like set

product the Sorts of S1 is non empty functional with_common_domain product-like set
S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
S2 | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
sproduct the Sorts of (c +* S1) is non empty functional set
S2 | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)

InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
() \/ () is set

InnerVertices y is non empty Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is non empty set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)

InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)

the carrier of (x +* y) is non empty set

the Sorts of (c +* S1) is Relation-like non-empty the carrier of (x +* y) -defined Function-like total set
product the Sorts of (c +* S1) is non empty functional with_common_domain product-like set
S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
S2 | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
sproduct the Sorts of (c +* S1) is non empty functional set
Following S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
() | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
A is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c
Following A is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c

product the Sorts of S1 is non empty functional with_common_domain product-like set
S2 | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
proj1 () is set
A1 is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1
Following A1 is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1
() +* () is Relation-like the carrier of y \/ the carrier of x -defined Function-like total set
the carrier of y \/ the carrier of x is non empty set

InnerVertices x is non empty Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)

InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is non empty set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)

the carrier of (x +* y) is non empty set

the Sorts of (c +* S1) is Relation-like non-empty the carrier of (x +* y) -defined Function-like total set
product the Sorts of (c +* S1) is non empty functional with_common_domain product-like set

product the Sorts of S1 is non empty functional with_common_domain product-like set
S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
S2 | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
sproduct the Sorts of (c +* S1) is non empty functional set
Following S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
() | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
A is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1
Following A is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1

S2 | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
proj1 () is set
A1 is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c
Following A1 is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c
() +* () is Relation-like the carrier of x \/ the carrier of y -defined Function-like total set
the carrier of x \/ the carrier of y is non empty set

InnerVertices y is non empty Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is non empty set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)

InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is