:: MSUALG_9 semantic presentation

NAT is non empty non trivial V24() V25() V26() non finite countable denumerable Element of bool REAL
REAL is set

NAT is non empty non trivial V24() V25() V26() non finite countable denumerable set

K214() is non empty V65() L9()
the carrier of K214() is non empty set
K217() is countable Element of bool NAT
[:K217(),K217():] is Relation-like set
[:[:K217(),K217():],K217():] is Relation-like set
bool [:[:K217(),K217():],K217():] is set
K284() is set

K155() is M8()

PFuncs (K155(),) is set
1 is non empty set
{{},1} is non empty finite countable set
K429() is set
bool K429() is set
K430() is Element of bool K429()
K470() is non empty strict DTConstrStr
the carrier of K470() is non empty set
K433( the carrier of K470()) is non empty M34( the carrier of K470())
K469(K470()) is Element of bool K433( the carrier of K470())
bool K433( the carrier of K470()) is set

bool [:K469(K470()),NAT:] is set

bool [:NAT,K469(K470()):] is set
S is set

Bool A is functional non empty with_common_domain V139(S,A) V140(S,A) V141(S,A) V142(S,A) V143(S,A) V144(S,A) Element of bool (Bool A)

bool (Bool A) is set

bool [:S,:] is set

S is set

B is set
A . B is set
the Element of A . B is Element of A . B
{ the Element of A . B} is non empty finite countable set
C1 is non empty finite countable set

F is set
B . F is set
A . F is set
C1 is set
G is Element of A . F
{G} is non empty finite countable set

C1 is set
F . C1 is set
A . C1 is set
G is Element of A . C1
{G} is non empty finite countable set
C1 is set
F . C1 is set
A . C1 is set
G is Element of A . C1
{G} is non empty finite countable set
S is non empty non void V54() ManySortedSign
the carrier' of S is non empty set
B is Element of the carrier' of S
A is non-empty MSAlgebra over S
Args (B,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
the carrier of S is non empty set

K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . B is set
F is Relation-like Function-like Element of Args (B,A)
dom F is set
the_arity_of B is Relation-like NAT -defined the carrier of S -valued Function-like FinSequence-like M9( the carrier of S,K155( the carrier of S))
the Arity of S . B is Element of K155( the carrier of S)

C1 is V24() V25() V26() V30() set

S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is set

B is Element of the carrier of S
() . B is non empty set
C1 is Element of () . B

S is non empty non void V54() ManySortedSign
the carrier of S is non empty set

FreeMSA A is strict non-empty MSAlgebra over S

S is non empty non void V54() ManySortedSign
the carrier of S is non empty set

FreeMSA A is strict non-empty MSAlgebra over S
S is non empty non void V54() ManySortedSign
A is non-empty MSAlgebra over S
B is non-empty MSAlgebra over S
[:A,B:] is strict MSAlgebra over S
the carrier of S is non empty set

[| the Sorts of A, the Sorts of B|] is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
the Charact of B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of B), the ResultSort of S * the Sorts of B
K158( the carrier of S, the Sorts of B) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S, the Sorts of B) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * the Sorts of B is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
[[: the Charact of A, the Charact of B:]] is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,[| the Sorts of A, the Sorts of B|]), the ResultSort of S * [| the Sorts of A, the Sorts of B|]
K158( the carrier of S,[| the Sorts of A, the Sorts of B|]) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,[| the Sorts of A, the Sorts of B|]) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * [| the Sorts of A, the Sorts of B|] is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# [| the Sorts of A, the Sorts of B|],[[: the Charact of A, the Charact of B:]] #) is strict MSAlgebra over S
the Sorts of [:A,B:] is Relation-like the carrier of S -defined Function-like non empty total set
S is set
A is set
B is set
[:A,B:] is Relation-like set

dom F is set
F . S is set

(pr1 F) . S is set

(pr2 F) . S is set
[((pr1 F) . S),((pr2 F) . S)] is V15() set
{((pr1 F) . S),((pr2 F) . S)} is non empty finite countable set
{((pr1 F) . S)} is non empty finite countable set
{{((pr1 F) . S),((pr2 F) . S)},{((pr1 F) . S)}} is non empty finite V35() countable set
(F . S) `1 is set
(F . S) `2 is set
S is non empty set
A is set
{A} is non empty finite countable set

bool [:S,{A}:] is set

rng B is non empty finite countable Element of bool {A}

F is set
C1 is set
dom B is non empty Element of bool S
bool S is set
B . C1 is set
S is set

[:S,S:] is Relation-like set
bool [:S,S:] is set

{S} is non empty finite countable set
A is set
B is set
Class ((),B) is Element of bool S
bool S is set
S is non empty set

[:S,S:] is Relation-like set
bool [:S,S:] is set
Class () is non empty with_non-empty_elements a_partition of S
{S} is non empty finite countable set
A is set
B is set
Class ((),A) is Element of bool S
bool S is set
S is set
A is set
{A} is non empty finite countable set

{{A}} is non empty finite V35() countable set

bool [:S,{{A}}:] is set

bool [:S,{A}:] is set

F is set

B . F is set
{(B . F)} is non empty finite countable set
(S --> {A}) . F is set
S is set

F is set
B . F is set
A . F is set
\/ (A . F) is non empty set

C1 is set
A . C1 is set
F . C1 is set
(A . C1) \/ is non empty set
S is set

F is set
A . F is set
the Element of A . F is Element of A . F
{ the Element of A . F} is non empty finite countable set

{ the Element of A . F} \/ (B . F) is non empty finite countable set
G is non empty finite countable set

C1 is set
F . C1 is set
A . C1 is set
B . C1 is finite countable set
G is Element of A . C1
{G} is non empty finite countable set
{G} \/ (B . C1) is non empty finite countable set
I is set
C1 is set
F . C1 is set
B . C1 is finite countable set
A . C1 is set
I is Element of A . C1
{I} is non empty finite countable set
{I} \/ (B . C1) is non empty finite countable set
C1 is set
F . C1 is set
A . C1 is set
B . C1 is finite countable set
G is Element of A . C1
{G} is non empty finite countable set
{G} \/ (B . C1) is non empty finite countable set

G is set

C1 . G is finite countable set
A . G is set
I is Element of A . G
{I} is non empty finite countable set
{I} \/ (B . G) is non empty finite countable set
S is set

G is set

B . G is set
{(B . G)} is non empty finite countable set

A . G is set
[:(A . G),({B} . G):] is Relation-like set
bool [:(A . G),({B} . G):] is set

S is set

C1 is set

rng (F . C1) is set

B . C1 is set
{(B . C1)} is non empty finite countable set
A . C1 is set
[:(A . C1),({B} . C1):] is Relation-like set
bool [:(A . C1),({B} . C1):] is set
S is set

C1 is set

A . C1 is set
{(A . C1)} is non empty finite countable set

B . C1 is set
[:({A} . C1),(B . C1):] is Relation-like set
bool [:({A} . C1),(B . C1):] is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set

DTConMSA A is non empty strict V175() V176() V177() DTConstrStr
F is set

C1 is Element of the carrier of S
() . C1 is Relation-like () . C1 -defined A . C1 -valued Function-like non empty total V18(() . C1,A . C1) Element of bool [:(() . C1),(A . C1):]
() . C1 is non empty set
A . C1 is non empty set
[:(() . C1),(A . C1):] is Relation-like set
bool [:(() . C1),(A . C1):] is set
I is set
dom (() . F) is set
sQ is set
(() . F) . I is set
(() . F) . sQ is set
FreeGen (C1,A) is non empty Element of bool (() . C1)

() . C1 is non empty set
bool (() . C1) is set
Reverse (C1,A) is Relation-like FreeGen (C1,A) -defined A . C1 -valued Function-like non empty total V18( FreeGen (C1,A),A . C1) Element of bool [:(FreeGen (C1,A)),(A . C1):]
[:(FreeGen (C1,A)),(A . C1):] is Relation-like set
bool [:(FreeGen (C1,A)),(A . C1):] is set
dom (() . C1) is non empty Element of bool (() . C1)
bool (() . C1) is set
sF is set
[sF,C1] is V15() set
{sF,C1} is non empty finite countable set
{sF} is non empty finite countable set
{{sF,C1},{sF}} is non empty finite V35() countable set

Terminals () is non empty Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () is set
C12 is Element of the carrier of ()
C12 `2 is set
root-tree C12 is Relation-like Function-like finite countable V164() Element of K433( the carrier of ())
K433( the carrier of ()) is non empty M34( the carrier of ())
{ () where b1 is Element of the carrier of () : ( b1 in Terminals () & b1 `2 = C1 ) } is set
(() . C1) . sQ is set
[sF,C1] `1 is set
H is set
[H,C1] is V15() set
{H,C1} is non empty finite countable set
{H} is non empty finite countable set
{{H,C1},{H}} is non empty finite V35() countable set

i is Element of the carrier of ()
i `2 is set

(() . C1) . I is set
[H,C1] `1 is set
S is set

is non empty finite countable set

bool is set

B is set

[:NAT,(A . B):] is Relation-like set
bool [:NAT,(A . B):] is set
F is Relation-like NAT -defined A . B -valued Function-like V18( NAT ,A . B) Element of bool [:NAT,(A . B):]
rng F is finite countable Element of bool (A . B)
bool (A . B) is finite V35() countable set

F is set
B . F is set
() . F is set

[:(() . F),(A . F):] is Relation-like set
bool [:(() . F),(A . F):] is set
[:NAT,(A . F):] is Relation-like set
bool [:NAT,(A . F):] is set
C1 is Relation-like NAT -defined A . F -valued Function-like V18( NAT ,A . F) Element of bool [:NAT,(A . F):]
rng C1 is finite countable Element of bool (A . F)
bool (A . F) is finite V35() countable set

C1 is set

rng (F . C1) is set
A . C1 is finite countable set
[:NAT,(A . C1):] is Relation-like set
bool [:NAT,(A . C1):] is set
G is Relation-like NAT -defined A . C1 -valued Function-like V18( NAT ,A . C1) Element of bool [:NAT,(A . C1):]
rng G is finite countable Element of bool (A . C1)
bool (A . C1) is finite V35() countable set
S is non empty V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S

B is Relation-like the carrier of S -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
F is Relation-like the carrier of S -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
dom B is non empty Element of bool the carrier of S
bool the carrier of S is set
dom the Sorts of A is non empty Element of bool the carrier of S
dom F is non empty Element of bool the carrier of S
G is set
proj ( the Sorts of A,G) is Relation-like product the Sorts of A -defined Function-like non empty total set
dom (proj ( the Sorts of A,G)) is functional non empty with_common_domain Element of bool (product the Sorts of A)
bool (product the Sorts of A) is set
B . G is set
(proj ( the Sorts of A,G)) . B is set
(proj ( the Sorts of A,G)) . F is set
F . G is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non empty set
B is Element of the carrier of S

C1 is Relation-like A -defined Function-like Carrier (F,B) -compatible non empty total Element of product (Carrier (F,B))
G is Relation-like A -defined Function-like Carrier (F,B) -compatible non empty total Element of product (Carrier (F,B))
dom C1 is non empty Element of bool A
bool A is set
dom (Carrier (F,B)) is non empty Element of bool A
dom G is non empty Element of bool A
I is set
proj ((Carrier (F,B)),I) is Relation-like product (Carrier (F,B)) -defined Function-like non empty total set
dom (proj ((Carrier (F,B)),I)) is functional non empty with_common_domain Element of bool (product (Carrier (F,B)))
bool (product (Carrier (F,B))) is set
C1 . I is set
(proj ((Carrier (F,B)),I)) . C1 is set
(proj ((Carrier (F,B)),I)) . G is set
G . I is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
B is non-empty MSAlgebra over S

F is non-empty MSSubAlgebra of A

C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of F
id the Sorts of F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of F
G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of A
G ** C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of A
I is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of A
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S

B is non-empty MSAlgebra over S

F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B

the Sorts of () is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of ()
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is non-empty MSAlgebra over S

B is non-empty MSAlgebra over S

F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
C1 is Element of the carrier' of S
Args (C1,B) is functional non empty Element of rng K158( the carrier of S, the Sorts of B)
K158( the carrier of S, the Sorts of B) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of B) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of B) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of B)) . C1 is set
Args (C1,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . C1 is set

the_arity_of C1 is Relation-like NAT -defined the carrier of S -valued Function-like FinSequence-like M9( the carrier of S,K155( the carrier of S))
the Arity of S . C1 is Element of K155( the carrier of S)
len () is V24() V25() V26() V30() Element of NAT
Seg (len ()) is countable Element of bool NAT
sQ is V24() V25() V26() V30() Element of NAT
() /. sQ is Element of the carrier of S
the Sorts of A . (() /. sQ) is non empty set
the Sorts of B . (() /. sQ) is non empty set
F . (() /. sQ) is Relation-like the Sorts of A . (() /. sQ) -defined the Sorts of B . (() /. sQ) -valued Function-like non empty total V18( the Sorts of A . (() /. sQ), the Sorts of B . (() /. sQ)) Element of bool [:( the Sorts of A . (() /. sQ)),( the Sorts of B . (() /. sQ)):]
[:( the Sorts of A . (() /. sQ)),( the Sorts of B . (() /. sQ)):] is Relation-like set
bool [:( the Sorts of A . (() /. sQ)),( the Sorts of B . (() /. sQ)):] is set
G . sQ is set

rng (F . (() /. sQ)) is non empty Element of bool ( the Sorts of B . (() /. sQ))
bool ( the Sorts of B . (() /. sQ)) is set
C12 is set
(F . (() /. sQ)) . C12 is set
H is Element of the Sorts of A . (() /. sQ)
(F . (() /. sQ)) . H is Element of the Sorts of B . (() /. sQ)

len sQ is V24() V25() V26() V30() Element of NAT
sF is V24() V25() V26() V30() set
sQ . sF is set
() /. sF is Element of the carrier of S
the Sorts of A . (() /. sF) is non empty set
the Sorts of B . (() /. sF) is non empty set
F . (() /. sF) is Relation-like the Sorts of A . (() /. sF) -defined the Sorts of B . (() /. sF) -valued Function-like non empty total V18( the Sorts of A . (() /. sF), the Sorts of B . (() /. sF)) Element of bool [:( the Sorts of A . (() /. sF)),( the Sorts of B . (() /. sF)):]
[:( the Sorts of A . (() /. sF)),( the Sorts of B . (() /. sF)):] is Relation-like set
bool [:( the Sorts of A . (() /. sF)),( the Sorts of B . (() /. sF)):] is set
G . sF is set
C12 is Element of the Sorts of A . (() /. sF)
(F . (() /. sF)) . C12 is Element of the Sorts of B . (() /. sF)

dom (() * the Sorts of B) is countable Element of bool NAT

i is V24() V25() V26() V30() set
(F # sF) . i is set
G . i is set
() /. i is Element of the carrier of S
the Sorts of A . (() /. i) is non empty set
the Sorts of B . (() /. i) is non empty set
F . (() /. i) is Relation-like the Sorts of A . (() /. i) -defined the Sorts of B . (() /. i) -valued Function-like non empty total V18( the Sorts of A . (() /. i), the Sorts of B . (() /. i)) Element of bool [:( the Sorts of A . (() /. i)),( the Sorts of B . (() /. i)):]
[:( the Sorts of A . (() /. i)),( the Sorts of B . (() /. i)):] is Relation-like set
bool [:( the Sorts of A . (() /. i)),( the Sorts of B . (() /. i)):] is set
sF . i is set
s is Element of the Sorts of A . (() /. i)
(F . (() /. i)) . s is Element of the Sorts of B . (() /. i)
dom (F # sF) is countable Element of bool NAT
S is non empty non void V54() ManySortedSign
the carrier' of S is non empty set
A is non-empty MSAlgebra over S

the carrier of S is non empty set
B is Element of the carrier' of S
Args (B,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . B is set
Result (B,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . B is non empty set
Den (B,A) is Relation-like Args (B,A) -defined Result (B,A) -valued Function-like non empty total V18( Args (B,A), Result (B,A)) Element of bool [:(Args (B,A)),(Result (B,A)):]
[:(Args (B,A)),(Result (B,A)):] is Relation-like set
bool [:(Args (B,A)),(Result (B,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . B is set
the_result_sort_of B is Element of the carrier of S
the ResultSort of S . B is Element of the carrier of S
the Sorts of A . is non empty set

(Den (B,A)) . F is Element of Result (B,A)
the Sorts of A . ( the ResultSort of S . B) is non empty set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S

B is non-empty MSAlgebra over S

F is non-empty MSAlgebra over S

C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of F
I is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of F
I ** C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of F
the carrier' of S is non empty set
sQ is Element of the carrier' of S
Args (sQ,B) is functional non empty Element of rng K158( the carrier of S, the Sorts of B)
K158( the carrier of S, the Sorts of B) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of B) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of B) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of B)) . sQ is set
the_result_sort_of sQ is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . sQ is Element of the carrier of S
I . () is Relation-like the Sorts of B . () -defined the Sorts of F . () -valued Function-like non empty total V18( the Sorts of B . (), the Sorts of F . ()) Element of bool [:( the Sorts of B . ()),( the Sorts of F . ()):]
the Sorts of B . () is non empty set
the Sorts of F . () is non empty set
[:( the Sorts of B . ()),( the Sorts of F . ()):] is Relation-like set
bool [:( the Sorts of B . ()),( the Sorts of F . ()):] is set
Den (sQ,B) is Relation-like Args (sQ,B) -defined Result (sQ,B) -valued Function-like non empty total V18( Args (sQ,B), Result (sQ,B)) Element of bool [:(Args (sQ,B)),(Result (sQ,B)):]
Result (sQ,B) is non empty Element of rng the Sorts of B
rng the Sorts of B is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of B is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of B) . sQ is non empty set
[:(Args (sQ,B)),(Result (sQ,B)):] is Relation-like set
bool [:(Args (sQ,B)),(Result (sQ,B)):] is set
the Charact of B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of B), the ResultSort of S * the Sorts of B
the Charact of B . sQ is set
Den (sQ,F) is Relation-like Args (sQ,F) -defined Result (sQ,F) -valued Function-like non empty total V18( Args (sQ,F), Result (sQ,F)) Element of bool [:(Args (sQ,F)),(Result (sQ,F)):]
Args (sQ,F) is functional non empty Element of rng K158( the carrier of S, the Sorts of F)
K158( the carrier of S, the Sorts of F) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of F) is set
the Arity of S * K158( the carrier of S, the Sorts of F) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of F)) . sQ is set
Result (sQ,F) is non empty Element of rng the Sorts of F
rng the Sorts of F is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of F is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of F) . sQ is non empty set
[:(Args (sQ,F)),(Result (sQ,F)):] is Relation-like set
bool [:(Args (sQ,F)),(Result (sQ,F)):] is set
the Charact of F is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of F), the ResultSort of S * the Sorts of F
the Charact of F . sQ is set

(Den (sQ,B)) . sF is set
(I . ()) . ((Den (sQ,B)) . sF) is set

(Den (sQ,F)) . (I # sF) is set
Args (sQ,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . sQ is set

C1 # C12 is Relation-like Function-like FinSequence-like Element of Args (sQ,B)
C1 . () is Relation-like the Sorts of A . () -defined the Sorts of B . () -valued Function-like non empty total V18( the Sorts of A . (), the Sorts of B . ()) Element of bool [:( the Sorts of A . ()),( the Sorts of B . ()):]
the Sorts of A . () is non empty set
[:( the Sorts of A . ()),( the Sorts of B . ()):] is Relation-like set
bool [:( the Sorts of A . ()),( the Sorts of B . ()):] is set
Result (sQ,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . sQ is non empty set
Den (sQ,A) is Relation-like Args (sQ,A) -defined Result (sQ,A) -valued Function-like non empty total V18( Args (sQ,A), Result (sQ,A)) Element of bool [:(Args (sQ,A)),(Result (sQ,A)):]
[:(Args (sQ,A)),(Result (sQ,A)):] is Relation-like set
bool [:(Args (sQ,A)),(Result (sQ,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . sQ is set
(Den (sQ,A)) . C12 is Element of Result (sQ,A)
(C1 . ()) . ((Den (sQ,A)) . C12) is set
(Den (sQ,B)) . sF is Element of Result (sQ,B)
G . () is Relation-like the Sorts of A . () -defined the Sorts of F . () -valued Function-like non empty total V18( the Sorts of A . (), the Sorts of F . ()) Element of bool [:( the Sorts of A . ()),( the Sorts of F . ()):]
[:( the Sorts of A . ()),( the Sorts of F . ()):] is Relation-like set
bool [:( the Sorts of A . ()),( the Sorts of F . ()):] is set
(G . ()) . ((Den (sQ,A)) . C12) is set
(I . ()) * (C1 . ()) is Relation-like the Sorts of A . () -defined the Sorts of F . () -valued Function-like non empty total V18( the Sorts of A . (), the Sorts of F . ()) Element of bool [:( the Sorts of A . ()),( the Sorts of F . ()):]
((I . ()) * (C1 . ())) . ((Den (sQ,A)) . C12) is set
(I . ()) . ((Den (sQ,B)) . sF) is set
(I ** C1) # C12 is Relation-like Function-like FinSequence-like Element of Args (sQ,F)
(Den (sQ,F)) . ((I ** C1) # C12) is Element of Result (sQ,F)
(Den (sQ,F)) . (I # sF) is Element of Result (sQ,F)
S is set

I is set
G . I is set
A . I is set
B . I is set
[:(A . I),(B . I):] is Relation-like set
bool [:(A . I),(B . I):] is set

pr1 (C1 . I) is Relation-like Function-like set
[|B,F|] . I is set
[:(A . I),([|B,F|] . I):] is Relation-like set
bool [:(A . I),([|B,F|] . I):] is set

rng sF is set
sQ is non empty set
C12 is set
dom sF is set
H is set
sF . H is set
dom (C1 . I) is set
(C1 . I) . H is set
((C1 . I) . H) `1 is set
rng (C1 . I) is set
F . I is set
[:(B . I),(F . I):] is Relation-like set
dom (C1 . I) is set
dom sF is set

sQ is set

pr1 (C1 . sQ) is Relation-like Function-like set

sQ is set

pr1 (C1 . sQ) is Relation-like Function-like set

I is set
G . I is set
A . I is set
F . I is set
[:(A . I),(F . I):] is Relation-like set
bool [:(A . I),(F . I):] is set

pr2 (C1 . I) is Relation-like Function-like set
[|B,F|] . I is set
[:(A . I),([|B,F|] . I):] is Relation-like set
bool [:(A . I),([|B,F|] . I):] is set

rng sF is set
sQ is non empty set
C12 is set
dom sF is set
H is set
sF . H is set
dom (C1 . I) is set
(C1 . I) . H is set
((C1 . I) . H) `2 is set
rng (C1 . I) is set
B . I is set
[:(B . I),(F . I):] is Relation-like set
dom (C1 . I) is set
dom sF is set

sQ is set

pr2 (C1 . sQ) is Relation-like Function-like set

sQ is set

pr2 (C1 . sQ) is Relation-like Function-like set

S is set
A is set
{A} is non empty finite countable set

{{A}} is non empty finite V35() countable set

bool [:S,{{A}}:] is set

(S,B,(S --> {A}),(S --> {A}),F) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of B,S --> {A}
(S,B,(S --> {A}),(S --> {A}),F) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of B,S --> {A}
C1 is set

pr2 (F . C1) is Relation-like Function-like set
dom (pr2 (F . C1)) is set
dom (F . C1) is set
G is set
(F . C1) . G is set
rng (F . C1) is set
B . C1 is set
[|(S --> {A}),(S --> {A})|] . C1 is set
[:(B . C1),([|(S --> {A}),(S --> {A})|] . C1):] is Relation-like set
bool [:(B . C1),([|(S --> {A}),(S --> {A})|] . C1):] is set
(S --> {A}) . C1 is set
[:((S --> {A}) . C1),((S --> {A}) . C1):] is Relation-like set
((F . C1) . G) `1 is set
((F . C1) . G) `2 is set
(pr2 (F . C1)) . G is set
(S,B,(S --> {A}),(S --> {A}),F) . C1 is Relation-like Function-like set
pr1 (F . C1) is Relation-like Function-like set
(S,B,(S --> {A}),(S --> {A}),F) . C1 is Relation-like Function-like set
S is set

G is set
(S,A,B,F,C1) . G is Relation-like Function-like set
rng ((S,A,B,F,C1) . G) is set
B . G is set
A . G is set
[:(A . G),(B . G):] is Relation-like set
bool [:(A . G),(B . G):] is set
I is Relation-like A . G -defined B . G -valued Function-like V18(A . G,B . G) Element of bool [:(A . G),(B . G):]
rng I is Element of bool (B . G)
bool (B . G) is set
sQ is set
[|B,F|] . G is set
sF is set
sF `2 is set
[sQ,(sF `2)] is V15() set
{sQ,(sF `2)} is non empty finite countable set
{sQ} is non empty finite countable set
{{sQ,(sF `2)},{sQ}} is non empty finite V35() countable set
F . G is set
[:(B . G),(F . G):] is Relation-like set
[sQ,(sF `2)] `2 is set
[sQ,(sF `2)] `1 is set
dom I is Element of bool (A . G)
bool (A . G) is set

[:(A . G),([|B,F|] . G):] is Relation-like set
bool [:(A . G),([|B,F|] . G):] is set
dom (C1 . G) is set
rng (C1 . G) is set
H is set
(C1 . G) . H is set
I . H is set
pr1 (C1 . G) is Relation-like Function-like set
(pr1 (C1 . G)) . H is set
S is set

G is set
(S,A,B,F,C1) . G is Relation-like Function-like set
rng ((S,A,B,F,C1) . G) is set
F . G is set
A . G is set
[:(A . G),(F . G):] is Relation-like set
bool [:(A . G),(F . G):] is set
I is Relation-like A . G -defined F . G -valued Function-like V18(A . G,F . G) Element of bool [:(A . G),(F . G):]
rng I is Element of bool (F . G)
bool (F . G) is set
sQ is set
[|B,F|] . G is set
sF is set
sF `1 is set
[(sF `1),sQ] is V15() set
{(sF `1),sQ} is non empty finite countable set
{(sF `1)} is non empty finite countable set
{{(sF `1),sQ},{(sF `1)}} is non empty finite V35() countable set
B . G is set
[:(B . G),(F . G):] is Relation-like set
[(sF `1),sQ] `1 is set
[(sF `1),sQ] `2 is set
dom I is Element of bool (A . G)
bool (A . G) is set

[:(A . G),([|B,F|] . G):] is Relation-like set
bool [:(A . G),([|B,F|] . G):] is set
dom (C1 . G) is set
rng (C1 . G) is set
H is set
(C1 . G) . H is set
I . H is set
pr2 (C1 . G) is Relation-like Function-like set
(pr2 (C1 . G)) . H is set
S is set

(S,A,F,C1,G) .. B is Relation-like S -defined Function-like total set

(S,A,F,C1,G) .. B is Relation-like S -defined Function-like total set
I is set
(G .. B) . I is set
((S,A,F,C1,G) .. B) . I is set
((S,A,F,C1,G) .. B) . I is set
[(((S,A,F,C1,G) .. B) . I),(((S,A,F,C1,G) .. B) . I)] is V15() set
{(((S,A,F,C1,G) .. B) . I),(((S,A,F,C1,G) .. B) . I)} is non empty finite countable set
{(((S,A,F,C1,G) .. B) . I)} is non empty finite countable set
{{(((S,A,F,C1,G) .. B) . I),(((S,A,F,C1,G) .. B) . I)},{(((S,A,F,C1,G) .. B) . I)}} is non empty finite V35() countable set
B . I is set
(doms G) . I is set

dom (G . I) is set
sQ is set
[|F,C1|] . sQ is set
A . sQ is set
[|F,C1|] . I is set
F . I is set
C1 . I is set
[:(F . I),(C1 . I):] is Relation-like set
(G . I) . (B . I) is set
(S,A,F,C1,G) . I is Relation-like Function-like set

(pr2 (G . I)) . (B . I) is set
((G . I) . (B . I)) `2 is set
(S,A,F,C1,G) . I is Relation-like Function-like set

(pr1 (G . I)) . (B . I) is set
((G . I) . (B . I)) `1 is set
S is non empty V54() ManySortedSign
Trivial_Algebra S is strict MSAlgebra over S
the Sorts of () is Relation-like the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set

the carrier of S --> is Relation-like non-empty non empty-yielding the carrier of S -defined -valued Function-like constant non empty total V18( the carrier of S,) Element of bool [: the carrier of S,:]
is non empty finite V35() countable set
[: the carrier of S,:] is Relation-like set
bool [: the carrier of S,:] is set

S is non empty V54() ManySortedSign
Trivial_Algebra S is strict MSAlgebra over S

the carrier of S is non empty set
A is set
the Sorts of () . A is finite countable set

S is non empty non void V54() ManySortedSign
the carrier of S is non empty set

the carrier' of S is non empty set
A is non-empty MSAlgebra over S

B is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of ()
F is Element of the carrier' of S
Args (F,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . F is set
the_result_sort_of F is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . F is Element of the carrier of S
B . is Relation-like the Sorts of A . -defined the Sorts of () . -valued Function-like non empty total V18( the Sorts of A . , the Sorts of () . ) Element of bool [:( the Sorts of A . ),( the Sorts of () . ):]
the Sorts of A . is non empty set
the Sorts of () . is non empty finite countable set
[:( the Sorts of A . ),( the Sorts of () . ):] is Relation-like set
bool [:( the Sorts of A . ),( the Sorts of () . ):] is set
Result (F,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . F is non empty set
Den (F,A) is Relation-like Args (F,A) -defined Result (F,A) -valued Function-like non empty total V18( Args (F,A), Result (F,A)) Element of bool [:(Args (F,A)),(Result (F,A)):]
[:(Args (F,A)),(Result (F,A)):] is Relation-like set
bool [:(Args (F,A)),(Result (F,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . F is set
Args (F,()) is functional non empty Element of rng K158( the carrier of S, the Sorts of ())
K158( the carrier of S, the Sorts of ()) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of ()) is set
the Arity of S * K158( the carrier of S, the Sorts of ()) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of ())) . F is set
Result (F,()) is non empty finite countable Element of rng the Sorts of ()
rng the Sorts of () is non empty V35() with_non-empty_elements set
the ResultSort of S * the Sorts of () is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of ()) . F is non empty set
Den (F,()) is Relation-like Args (F,()) -defined Result (F,()) -valued Function-like non empty total V18( Args (F,()), Result (F,())) Element of bool [:(Args (F,())),(Result (F,())):]
[:(Args (F,())),(Result (F,())):] is Relation-like set
bool [:(Args (F,())),(Result (F,())):] is set
the Charact of () is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of ()), the ResultSort of S * the Sorts of ()
the Charact of () . F is set

(Den (F,A)) . C1 is Element of Result (F,A)
(B . ) . ((Den (F,A)) . C1) is set

(Den (F,())) . (B # C1) is Element of Result (F,())
H is set
the Sorts of () . H is finite countable set

the carrier of S --> is Relation-like non-empty non empty-yielding the carrier of S -defined -valued Function-like constant non empty total V18( the carrier of S,) Element of bool [: the carrier of S,:]
is non empty finite V35() countable set
[: the carrier of S,:] is Relation-like set
bool [: the carrier of S,:] is set

i is Element of the Sorts of A .
(B . ) . i is Element of the Sorts of () .
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set

A is non-empty MSAlgebra over S

B is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of ()

the carrier of S --> is Relation-like non-empty non empty-yielding the carrier of S -defined -valued Function-like constant non empty total V18( the carrier of S,) Element of bool [: the carrier of S,:]
is non empty finite V35() countable set
[: the carrier of S,:] is Relation-like set
bool [: the carrier of S,:] is set

the carrier' of S is non empty set
G is Element of the carrier' of S
Args (G,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . G is set
the_result_sort_of G is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . G is Element of the carrier of S
B . is Relation-like the Sorts of A . -defined the Sorts of () . -valued Function-like non empty total V18( the Sorts of A . , the Sorts of () . ) Element of bool [:( the Sorts of A . ),( the Sorts of () . ):]
the Sorts of A . is non empty set
the Sorts of () . is non empty finite countable set
[:( the Sorts of A . ),( the Sorts of () . ):] is Relation-like set
bool [:( the Sorts of A . ),( the Sorts of () . ):] is set
Den (G,A) is Relation-like Args (G,A) -defined Result (G,A) -valued Function-like non empty total V18( Args (G,A), Result (G,A)) Element of bool [:(Args (G,A)),(Result (G,A)):]
Result (G,A) is non empty Element of