:: MSUALG_9 semantic presentation

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

REAL is set

bool REAL is set

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

bool NAT is set

bool NAT is set

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

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

bool [:[:NAT,NAT:],NAT:] is 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

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable set

{{}} is functional non empty finite V35() with_common_domain countable set

K155({{}}) is M8({{}})

[:K155({{}}),{{}}:] is Relation-like set

bool [:K155({{}}),{{}}:] is set

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

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

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

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

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

S is set

A is Relation-like S -defined Function-like total 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 A is functional non empty with_common_domain set

bool (Bool A) is set

[[0]] S is Relation-like empty-yielding S -defined Function-like total finite-yielding set

S --> {} is Relation-like S -defined {{}} -valued Function-like constant total V18(S,{{}}) Function-yielding Relation-yielding Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

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

B is Relation-like S -defined Function-like total Element of Bool A

S is set

A is Relation-like non-empty S -defined Function-like total 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

B is Relation-like S -defined Function-like total 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

F is Relation-like S -defined Function-like total ManySortedSubset of A

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

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total 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)

dom (the_arity_of B) is countable Element of bool NAT

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

Seg C1 is countable Element of bool NAT

S is non empty non void V54() ManySortedSign

the carrier of S is non empty set

A is set

F is Relation-like A -defined Function-like total MSAlgebra-Family of A,S

SORTS F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

B is Element of the carrier of S

(SORTS F) . B is non empty set

C1 is Element of (SORTS F) . B

Carrier (F,B) is Relation-like non-empty A -defined Function-like total set

product (Carrier (F,B)) is functional non empty with_common_domain product-like set

S is non empty non void V54() ManySortedSign

the carrier of S is non empty set

A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

FreeMSA A is strict non-empty MSAlgebra over S

FreeGen A is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of FreeMSA A

S is non empty non void V54() ManySortedSign

the carrier of S is non empty set

A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total 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 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total 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

F is Relation-like Function-like set

dom F is set

F . S is set

pr1 F is Relation-like Function-like set

(pr1 F) . S is set

pr2 F is Relation-like Function-like 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

[:S,{A}:] is Relation-like set

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

B is Relation-like S -defined {A} -valued Function-like non empty total V18(S,{A}) Element of bool [:S,{A}:]

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

bool {A} is finite V35() countable set

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

nabla S is Relation-like S -defined S -valued total V18(S,S) reflexive symmetric transitive Element of bool [:S,S:]

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

bool [:S,S:] is set

Class (nabla S) is with_non-empty_elements a_partition of S

{S} is non empty finite countable set

A is set

B is set

Class ((nabla S),B) is Element of bool S

bool S is set

S is non empty set

nabla S is Relation-like S -defined S -valued total V18(S,S) reflexive symmetric transitive Element of bool [:S,S:]

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

bool [:S,S:] is set

Class (nabla S) 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 ((nabla S),A) is Element of bool S

bool S is set

S is set

A is set

{A} is non empty finite countable set

S --> {A} is Relation-like non-empty S -defined {{A}} -valued Function-like constant total V18(S,{{A}}) Element of bool [:S,{{A}}:]

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

[:S,{{A}}:] is Relation-like set

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

S --> A is Relation-like S -defined {A} -valued Function-like constant total V18(S,{A}) Element of bool [:S,{A}:]

[:S,{A}:] is Relation-like set

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

B is Relation-like S -defined Function-like total set

{B} is Relation-like non-empty S -defined Function-like total finite-yielding set

F is set

{B} . F is finite countable set

B . F is set

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

(S --> {A}) . F is set

S is set

A is Relation-like S -defined Function-like total set

B is Relation-like S -defined Function-like total set

F is set

B . F is set

A . F is set

{{}} \/ (A . F) is non empty set

F is Relation-like non-empty S -defined Function-like total set

C1 is set

A . C1 is set

F . C1 is set

(A . C1) \/ {{}} is non empty set

S is set

A is Relation-like non-empty S -defined Function-like total set

B is Relation-like S -defined Function-like total finite-yielding ManySortedSubset of A

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

B . F is finite countable set

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

G is non empty finite countable set

F is Relation-like S -defined Function-like total 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

C1 is Relation-like non-empty S -defined Function-like total finite-yielding ManySortedSubset of A

G is set

B . G is finite countable 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

A is Relation-like S -defined Function-like total set

B is Relation-like S -defined Function-like total set

{B} is Relation-like non-empty S -defined Function-like total finite-yielding set

F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,{B}

C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,{B}

G is set

{B} . G is finite countable set

B . G is set

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

F . G is Relation-like Function-like set

A . G is set

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

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

C1 . G is Relation-like Function-like set

S is set

A is Relation-like non-empty S -defined Function-like total set

B is Relation-like S -defined Function-like total set

{B} is Relation-like non-empty S -defined Function-like total finite-yielding set

F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,{B}

C1 is set

F . C1 is Relation-like Function-like set

rng (F . C1) is set

{B} . C1 is finite countable 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

A is Relation-like S -defined Function-like total set

{A} is Relation-like non-empty S -defined Function-like total finite-yielding set

B is Relation-like non-empty S -defined Function-like total set

F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of {A},B

C1 is set

{A} . C1 is finite countable set

A . C1 is set

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

F . C1 is Relation-like Function-like 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

A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

Reverse A is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of FreeGen A,A

FreeGen A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total free GeneratorSet of FreeMSA A

FreeMSA A is strict non-empty free MSAlgebra over S

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

F is set

(Reverse A) . F is Relation-like Function-like set

C1 is Element of the carrier of S

(Reverse A) . C1 is Relation-like (FreeGen A) . C1 -defined A . C1 -valued Function-like non empty total V18((FreeGen A) . C1,A . C1) Element of bool [:((FreeGen A) . C1),(A . C1):]

(FreeGen A) . C1 is non empty set

A . C1 is non empty set

[:((FreeGen A) . C1),(A . C1):] is Relation-like set

bool [:((FreeGen A) . C1),(A . C1):] is set

I is set

dom ((Reverse A) . F) is set

sQ is set

((Reverse A) . F) . I is set

((Reverse A) . F) . sQ is set

FreeGen (C1,A) is non empty Element of bool ((FreeSort A) . C1)

FreeSort A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

(FreeSort A) . C1 is non empty set

bool ((FreeSort A) . 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 ((Reverse A) . C1) is non empty Element of bool ((FreeGen A) . C1)

bool ((FreeGen A) . 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

root-tree [sF,C1] is Relation-like Function-like finite countable V164() set

Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)

the carrier of (DTConMSA A) is non empty set

bool the carrier of (DTConMSA A) is set

C12 is Element of the carrier of (DTConMSA A)

C12 `2 is set

root-tree C12 is Relation-like Function-like finite countable V164() Element of K433( the carrier of (DTConMSA A))

K433( the carrier of (DTConMSA A)) is non empty M34( the carrier of (DTConMSA A))

{ (root-tree b

((Reverse A) . 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

root-tree [H,C1] is Relation-like Function-like finite countable V164() set

i is Element of the carrier of (DTConMSA A)

i `2 is set

root-tree i is Relation-like Function-like finite countable V164() Element of K433( the carrier of (DTConMSA A))

((Reverse A) . C1) . I is set

[H,C1] `1 is set

S is set

S --> NAT is Relation-like non-empty S -defined {NAT} -valued Function-like constant total V18(S,{NAT}) Element of bool [:S,{NAT}:]

{NAT} is non empty finite countable set

[:S,{NAT}:] is Relation-like set

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

A is Relation-like non-empty S -defined Function-like total finite-yielding set

B is set

A . B is finite countable 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

B is Relation-like S -defined Function-like total set

F is set

B . F is set

(S --> NAT) . F is set

A . F is finite countable set

[:((S --> NAT) . F),(A . F):] is Relation-like set

bool [:((S --> NAT) . 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

F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S --> NAT,A

C1 is set

F . C1 is Relation-like Function-like 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

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

product the Sorts of A is functional non empty with_common_domain product-like set

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

F is Relation-like A -defined Function-like non empty total MSAlgebra-Family of A,S

Carrier (F,B) is Relation-like non-empty non empty-yielding A -defined Function-like non empty total set

product (Carrier (F,B)) is functional non empty with_common_domain product-like set

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

the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

F is non-empty MSSubAlgebra of A

the Sorts of F 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 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

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

B is non-empty MSAlgebra over S

the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

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

Image F is strict non-empty MSSubAlgebra of B

the Sorts of (Image F) 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 (Image F)

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

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

B is non-empty MSAlgebra over S

the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

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

G is Relation-like Function-like FinSequence-like Element of Args (C1,B)

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 (the_arity_of C1) is V24() V25() V26() V30() Element of NAT

Seg (len (the_arity_of C1)) is countable Element of bool NAT

sQ is V24() V25() V26() V30() Element of NAT

(the_arity_of C1) /. sQ is Element of the carrier of S

the Sorts of A . ((the_arity_of C1) /. sQ) is non empty set

the Sorts of B . ((the_arity_of C1) /. sQ) is non empty set

F . ((the_arity_of C1) /. sQ) is Relation-like the Sorts of A . ((the_arity_of C1) /. sQ) -defined the Sorts of B . ((the_arity_of C1) /. sQ) -valued Function-like non empty total V18( the Sorts of A . ((the_arity_of C1) /. sQ), the Sorts of B . ((the_arity_of C1) /. sQ)) Element of bool [:( the Sorts of A . ((the_arity_of C1) /. sQ)),( the Sorts of B . ((the_arity_of C1) /. sQ)):]

[:( the Sorts of A . ((the_arity_of C1) /. sQ)),( the Sorts of B . ((the_arity_of C1) /. sQ)):] is Relation-like set

bool [:( the Sorts of A . ((the_arity_of C1) /. sQ)),( the Sorts of B . ((the_arity_of C1) /. sQ)):] is set

G . sQ is set

dom (the_arity_of C1) is countable Element of bool NAT

rng (F . ((the_arity_of C1) /. sQ)) is non empty Element of bool ( the Sorts of B . ((the_arity_of C1) /. sQ))

bool ( the Sorts of B . ((the_arity_of C1) /. sQ)) is set

C12 is set

(F . ((the_arity_of C1) /. sQ)) . C12 is set

H is Element of the Sorts of A . ((the_arity_of C1) /. sQ)

(F . ((the_arity_of C1) /. sQ)) . H is Element of the Sorts of B . ((the_arity_of C1) /. sQ)

sQ is Relation-like Function-like FinSequence-like set

dom sQ is countable Element of bool NAT

len sQ is V24() V25() V26() V30() Element of NAT

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

sQ . sF is set

(the_arity_of C1) /. sF is Element of the carrier of S

the Sorts of A . ((the_arity_of C1) /. sF) is non empty set

the Sorts of B . ((the_arity_of C1) /. sF) is non empty set

F . ((the_arity_of C1) /. sF) is Relation-like the Sorts of A . ((the_arity_of C1) /. sF) -defined the Sorts of B . ((the_arity_of C1) /. sF) -valued Function-like non empty total V18( the Sorts of A . ((the_arity_of C1) /. sF), the Sorts of B . ((the_arity_of C1) /. sF)) Element of bool [:( the Sorts of A . ((the_arity_of C1) /. sF)),( the Sorts of B . ((the_arity_of C1) /. sF)):]

[:( the Sorts of A . ((the_arity_of C1) /. sF)),( the Sorts of B . ((the_arity_of C1) /. sF)):] is Relation-like set

bool [:( the Sorts of A . ((the_arity_of C1) /. sF)),( the Sorts of B . ((the_arity_of C1) /. sF)):] is set

G . sF is set

C12 is Element of the Sorts of A . ((the_arity_of C1) /. sF)

(F . ((the_arity_of C1) /. sF)) . C12 is Element of the Sorts of B . ((the_arity_of C1) /. sF)

sF is Relation-like Function-like FinSequence-like Element of Args (C1,A)

F # sF is Relation-like Function-like FinSequence-like Element of Args (C1,B)

dom (the_arity_of C1) is countable Element of bool NAT

(the_arity_of C1) * the Sorts of B is Relation-like non-empty NAT -defined dom (the_arity_of C1) -defined Function-like total set

H is Relation-like non-empty dom (the_arity_of C1) -defined Function-like total set

product H is functional non empty with_common_domain product-like set

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

dom G is countable Element of bool NAT

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

(F # sF) . i is set

G . i is set

(the_arity_of C1) /. i is Element of the carrier of S

the Sorts of A . ((the_arity_of C1) /. i) is non empty set

the Sorts of B . ((the_arity_of C1) /. i) is non empty set

F . ((the_arity_of C1) /. i) is Relation-like the Sorts of A . ((the_arity_of C1) /. i) -defined the Sorts of B . ((the_arity_of C1) /. i) -valued Function-like non empty total V18( the Sorts of A . ((the_arity_of C1) /. i), the Sorts of B . ((the_arity_of C1) /. i)) Element of bool [:( the Sorts of A . ((the_arity_of C1) /. i)),( the Sorts of B . ((the_arity_of C1) /. i)):]

[:( the Sorts of A . ((the_arity_of C1) /. i)),( the Sorts of B . ((the_arity_of C1) /. i)):] is Relation-like set

bool [:( the Sorts of A . ((the_arity_of C1) /. i)),( the Sorts of B . ((the_arity_of C1) /. i)):] is set

sF . i is set

s is Element of the Sorts of A . ((the_arity_of C1) /. i)

(F . ((the_arity_of C1) /. i)) . s is Element of the Sorts of B . ((the_arity_of C1) /. 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 Sorts of A 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

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 . (the_result_sort_of B) is non empty set

F is Relation-like Function-like FinSequence-like Element of Args (B,A)

(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

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

B is non-empty MSAlgebra over S

the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

F is non-empty MSAlgebra over S

the Sorts of F 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 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 . (the_result_sort_of sQ) is Relation-like the Sorts of B . (the_result_sort_of sQ) -defined the Sorts of F . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of B . (the_result_sort_of sQ), the Sorts of F . (the_result_sort_of sQ)) Element of bool [:( the Sorts of B . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):]

the Sorts of B . (the_result_sort_of sQ) is non empty set

the Sorts of F . (the_result_sort_of sQ) is non empty set

[:( the Sorts of B . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] is Relation-like set

bool [:( the Sorts of B . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] 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

sF is Relation-like Function-like FinSequence-like Element of Args (sQ,B)

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

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

I # sF is Relation-like Function-like FinSequence-like Element of Args (sQ,F)

(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

C12 is Relation-like Function-like FinSequence-like Element of Args (sQ,A)

C1 # C12 is Relation-like Function-like FinSequence-like Element of Args (sQ,B)

C1 . (the_result_sort_of sQ) is Relation-like the Sorts of A . (the_result_sort_of sQ) -defined the Sorts of B . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of sQ), the Sorts of B . (the_result_sort_of sQ)) Element of bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of B . (the_result_sort_of sQ)):]

the Sorts of A . (the_result_sort_of sQ) is non empty set

[:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of B . (the_result_sort_of sQ)):] is Relation-like set

bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of B . (the_result_sort_of sQ)):] 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 . (the_result_sort_of sQ)) . ((Den (sQ,A)) . C12) is set

(Den (sQ,B)) . sF is Element of Result (sQ,B)

G . (the_result_sort_of sQ) is Relation-like the Sorts of A . (the_result_sort_of sQ) -defined the Sorts of F . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of sQ), the Sorts of F . (the_result_sort_of sQ)) Element of bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):]

[:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] is Relation-like set

bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] is set

(G . (the_result_sort_of sQ)) . ((Den (sQ,A)) . C12) is set

(I . (the_result_sort_of sQ)) * (C1 . (the_result_sort_of sQ)) is Relation-like the Sorts of A . (the_result_sort_of sQ) -defined the Sorts of F . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of sQ), the Sorts of F . (the_result_sort_of sQ)) Element of bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):]

((I . (the_result_sort_of sQ)) * (C1 . (the_result_sort_of sQ))) . ((Den (sQ,A)) . C12) is set

(I . (the_result_sort_of sQ)) . ((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

A is Relation-like S -defined Function-like total set

B is Relation-like non-empty S -defined Function-like total set

F is Relation-like non-empty S -defined Function-like total set

[|B,F|] is Relation-like non-empty S -defined Function-like total set

C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|B,F|]

G is Relation-like S -defined Function-like total 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

C1 . I is Relation-like Function-like 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

sF is Relation-like Function-like 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

I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,B

sQ is set

I . sQ is Relation-like Function-like set

C1 . sQ is Relation-like Function-like set

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

G is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,B

I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,B

sQ is set

G . sQ is Relation-like Function-like set

C1 . sQ is Relation-like Function-like set

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

I . sQ is Relation-like Function-like set

G is Relation-like S -defined Function-like total 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

C1 . I is Relation-like Function-like 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

sF is Relation-like Function-like 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

I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F

sQ is set

I . sQ is Relation-like Function-like set

C1 . sQ is Relation-like Function-like set

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

G is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F

I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F

sQ is set

G . sQ is Relation-like Function-like set

C1 . sQ is Relation-like Function-like set

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

I . sQ is Relation-like Function-like set

S is set

A is set

{A} is non empty finite countable set

S --> {A} is Relation-like non-empty S -defined {{A}} -valued Function-like constant total V18(S,{{A}}) Element of bool [:S,{{A}}:]

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

[:S,{{A}}:] is Relation-like set

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

[|(S --> {A}),(S --> {A})|] is Relation-like non-empty S -defined Function-like total set

B is Relation-like S -defined Function-like total set

F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of B,[|(S --> {A}),(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}

(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

F . C1 is Relation-like Function-like 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

A is Relation-like S -defined Function-like total set

B is Relation-like non-empty S -defined Function-like total set

F is Relation-like non-empty S -defined Function-like total set

[|B,F|] is Relation-like non-empty S -defined Function-like total set

C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|B,F|]

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

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

C1 . G is Relation-like Function-like 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

A is Relation-like S -defined Function-like total set

B is Relation-like non-empty S -defined Function-like total set

F is Relation-like non-empty S -defined Function-like total set

[|B,F|] is Relation-like non-empty S -defined Function-like total set

C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|B,F|]

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

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

C1 . G is Relation-like Function-like 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

A is Relation-like S -defined Function-like total set

B is Relation-like S -defined Function-like total set

F is Relation-like non-empty S -defined Function-like total set

C1 is Relation-like non-empty S -defined Function-like total set

[|F,C1|] is Relation-like non-empty S -defined Function-like total set

G is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|F,C1|]

doms G is Relation-like S -defined Function-like total set

G .. B is Relation-like S -defined Function-like total set

(S,A,F,C1,G) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F

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

(S,A,F,C1,G) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,C1

(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

G . I is Relation-like Function-like 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) 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) 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 (Trivial_Algebra S) is Relation-like the carrier of S -defined Function-like non empty total set

the carrier of S is non empty set

0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable Element of NAT

{0} is functional non empty finite V35() with_common_domain countable set

the carrier of S --> {0} is Relation-like non-empty non empty-yielding the carrier of S -defined {{0}} -valued Function-like constant non empty total V18( the carrier of S,{{0}}) Element of bool [: the carrier of S,{{0}}:]

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

[: the carrier of S,{{0}}:] is Relation-like set

bool [: the carrier of S,{{0}}:] is set

A is Relation-like the carrier of S -defined Function-like non empty total set

{A} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set

S is non empty V54() ManySortedSign

Trivial_Algebra S is strict MSAlgebra over S

the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set

the carrier of S is non empty set

A is set

the Sorts of (Trivial_Algebra S) . A is finite countable set

0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable Element of NAT

S is non empty non void V54() ManySortedSign

the carrier of S is non empty set

Trivial_Algebra S is strict non-empty finite-yielding MSAlgebra over S

the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set

the carrier' of S is non empty set

A is non-empty MSAlgebra over S

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

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 (Trivial_Algebra S)

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 . (the_result_sort_of F) is Relation-like the Sorts of A . (the_result_sort_of F) -defined the Sorts of (Trivial_Algebra S) . (the_result_sort_of F) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of F), the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)) Element of bool [:( the Sorts of A . (the_result_sort_of F)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)):]

the Sorts of A . (the_result_sort_of F) is non empty set

the Sorts of (Trivial_Algebra S) . (the_result_sort_of F) is non empty finite countable set

[:( the Sorts of A . (the_result_sort_of F)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)):] is Relation-like set

bool [:( the Sorts of A . (the_result_sort_of F)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)):] 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,(Trivial_Algebra S)) is functional non empty Element of rng K158( the carrier of S, the Sorts of (Trivial_Algebra S))

K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is Relation-like K155( the carrier of S) -defined Function-like total set

rng K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is set

the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is Relation-like the carrier' of S -defined Function-like set

( the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S))) . F is set

Result (F,(Trivial_Algebra S)) is non empty finite countable Element of rng the Sorts of (Trivial_Algebra S)

rng the Sorts of (Trivial_Algebra S) is non empty V35() with_non-empty_elements set

the ResultSort of S * the Sorts of (Trivial_Algebra S) 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 (Trivial_Algebra S)) . F is non empty set

Den (F,(Trivial_Algebra S)) is Relation-like Args (F,(Trivial_Algebra S)) -defined Result (F,(Trivial_Algebra S)) -valued Function-like non empty total V18( Args (F,(Trivial_Algebra S)), Result (F,(Trivial_Algebra S))) Element of bool [:(Args (F,(Trivial_Algebra S))),(Result (F,(Trivial_Algebra S))):]

[:(Args (F,(Trivial_Algebra S))),(Result (F,(Trivial_Algebra S))):] is Relation-like set

bool [:(Args (F,(Trivial_Algebra S))),(Result (F,(Trivial_Algebra S))):] is set

the Charact of (Trivial_Algebra S) 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 (Trivial_Algebra S)), the ResultSort of S * the Sorts of (Trivial_Algebra S)

the Charact of (Trivial_Algebra S) . F is set

C1 is Relation-like Function-like FinSequence-like Element of Args (F,A)

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

(B . (the_result_sort_of F)) . ((Den (F,A)) . C1) is set

B # C1 is Relation-like Function-like FinSequence-like Element of Args (F,(Trivial_Algebra S))

(Den (F,(Trivial_Algebra S))) . (B # C1) is Element of Result (F,(Trivial_Algebra S))

H is set

the Sorts of (Trivial_Algebra S) . H is finite countable set

{0} is functional non empty finite V35() with_common_domain countable set

the carrier of S --> {0} is Relation-like non-empty non empty-yielding the carrier of S -defined {{0}} -valued Function-like constant non empty total V18( the carrier of S,{{0}}) Element of bool [: the carrier of S,{{0}}:]

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

[: the carrier of S,{{0}}:] is Relation-like set

bool [: the carrier of S,{{0}}:] is set

s is Relation-like the carrier of S -defined Function-like non empty total set

{s} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set

i is Element of the Sorts of A . (the_result_sort_of F)

(B . (the_result_sort_of F)) . i is Element of the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)

S is non empty non void V54() ManySortedSign

the carrier of S is non empty set

Trivial_Algebra S is strict non-empty finite-yielding MSAlgebra over S

the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set

A is non-empty MSAlgebra over S

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

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 (Trivial_Algebra S)

{0} is functional non empty finite V35() with_common_domain countable set

the carrier of S --> {0} is Relation-like non-empty non empty-yielding the carrier of S -defined {{0}} -valued Function-like constant non empty total V18( the carrier of S,{{0}}) Element of bool [: the carrier of S,{{0}}:]

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

[: the carrier of S,{{0}}:] is Relation-like set

bool [: the carrier of S,{{0}}:] is set

C1 is Relation-like the carrier of S -defined Function-like non empty total set

{C1} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding 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 . (the_result_sort_of G) is Relation-like the Sorts of A . (the_result_sort_of G) -defined the Sorts of (Trivial_Algebra S) . (the_result_sort_of G) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of G), the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)) Element of bool [:( the Sorts of A . (the_result_sort_of G)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)):]

the Sorts of A . (the_result_sort_of G) is non empty set

the Sorts of (Trivial_Algebra S) . (the_result_sort_of G) is non empty finite countable set

[:( the Sorts of A . (the_result_sort_of G)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)):] is Relation-like set

bool [:( the Sorts of A . (the_result_sort_of G)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)):] 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