:: PRALG_3 semantic presentation

K160() is V40() countable denumerable Element of K10(K156())

K156() is set

K10(K156()) is non empty set

K109() is V40() countable denumerable set

K10(K109()) is non empty set

K10(K160()) is non empty set

K205() is set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() set

{{}} is non empty functional with_common_domain set

K183({{}}) is M10({{}})

K11(K183({{}}),{{}}) is Relation-like set

K10(K11(K183({{}}),{{}})) is non empty set

PFuncs (K183({{}}),{{}}) is non empty functional set

1 is non empty set

K11(1,1) is non empty Relation-like set

K10(K11(1,1)) is non empty set

K11(K11(1,1),1) is non empty Relation-like set

K10(K11(K11(1,1),1)) is non empty set

product {} is non empty functional with_common_domain product-like set

doms {} is Relation-like Function-like set

rngs {} is Relation-like Function-like set

I is set

S is non empty non void V68() ManySortedSign

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

product A is strict MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the carrier' of S is non empty set

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

I is with_non-empty_elements set

id I is Relation-like I -defined I -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(I,I))

K11(I,I) is Relation-like set

K10(K11(I,I)) is non empty set

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

A is set

S . A is set

I is Relation-like Function-like set

S is Relation-like Function-like set

product S is functional with_common_domain product-like set

A is set

I | A is Relation-like Function-like set

S | A is Relation-like Function-like set

product (S | A) is functional with_common_domain product-like set

dom I is set

dom S is set

dom (I | A) is set

(dom S) /\ A is set

dom (S | A) is set

EqR is set

(I | A) . EqR is set

(S | A) . EqR is set

S . EqR is set

I . EqR is set

I is non empty set

K10(I) is non empty set

S is non empty non void V68() ManySortedSign

the carrier of S is non empty set

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

EqR is Element of the carrier of S

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

U1 is non empty Element of K10(I)

A | U1 is Relation-like U1 -defined I -defined Function-like set

(Carrier (A,EqR)) | U1 is Relation-like U1 -defined I -defined Function-like set

U2 is non empty Relation-like U1 -defined Function-like total MSAlgebra-Family of U1,S

Carrier (U2,EqR) is non empty Relation-like non-empty non empty-yielding U1 -defined Function-like total set

dom ((Carrier (A,EqR)) | U1) is Element of K10(U1)

K10(U1) is non empty set

dom (Carrier (A,EqR)) is non empty Element of K10(I)

(dom (Carrier (A,EqR))) /\ U1 is Element of K10(I)

I /\ U1 is Element of K10(I)

U19 is non empty Relation-like U1 -defined Function-like total set

U29 is set

(Carrier (U2,EqR)) . U29 is set

U19 . U29 is set

F is Element of U1

U2 . F is non-empty MSAlgebra over S

A . F is non-empty MSAlgebra over S

s is Element of I

A . s is non-empty MSAlgebra over S

(Carrier (A,EqR)) . s is non empty set

U2 . U29 is set

s9 is MSAlgebra over S

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

the Sorts of s9 . EqR is set

f is MSAlgebra over S

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

the Sorts of f . EqR is set

I is set

S is non empty set

K11(S,S) is non empty Relation-like set

K10(K11(S,S)) is non empty set

K10(S) is non empty set

A is Relation-like S -defined S -valued V12() V14() V19() total Element of K10(K11(S,S))

Class A is non empty with_non-empty_elements non empty-membered a_partition of S

EqR is non empty Element of Class A

U1 is non empty Element of Class A

U2 is set

Class (A,U2) is Element of K10(S)

[I,U2] is set

{I,U2} is non empty set

{I} is non empty set

{{I,U2},{I}} is non empty with_non-empty_elements non empty-membered set

U19 is set

Class (A,U19) is Element of K10(S)

[I,U19] is set

{I,U19} is non empty set

{{I,U19},{I}} is non empty with_non-empty_elements non empty-membered set

Class (A,I) is Element of K10(S)

S is set

I is Relation-like Function-like set

product I is functional with_common_domain product-like set

I is non empty set

S is non empty Relation-like I -defined Function-like total Function-yielding V54() set

rng S is non empty set

commute S is Relation-like Function-like Function-yielding V54() set

{ (rng (S . b

union { (rng (S . b

U1 is non empty functional with_common_domain set

DOM U1 is set

EqR is Relation-like Function-like set

rng EqR is set

Funcs ((DOM U1),(union { (rng (S . b

U2 is set

dom S is non empty Element of K10(I)

K10(I) is non empty set

U19 is set

S . U19 is Relation-like Function-like set

U29 is Element of I

S . U29 is Relation-like Function-like set

F is Relation-like Function-like set

rng F is set

s is set

dom F is set

U2 is Element of I

S . U2 is Relation-like Function-like set

U19 is set

(S . U2) . U19 is set

(commute S) . U19 is Relation-like Function-like set

((commute S) . U19) . U2 is set

dom EqR is set

Funcs (I,(Funcs ((DOM U1),(union { (rng (S . b

I is non empty non void V68() ManySortedSign

the carrier' of I is non empty set

A is Element of the carrier' of I

S is MSAlgebra over I

Den (A,S) is Relation-like Args (A,S) -defined Result (A,S) -valued Function-like quasi_total Element of K10(K11((Args (A,S)),(Result (A,S))))

Args (A,S) is Element of rng K186( the carrier of I, the Sorts of S)

the carrier of I is non empty set

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

K186( the carrier of I, the Sorts of S) is Relation-like K183( the carrier of I) -defined Function-like total set

K183( the carrier of I) is M10( the carrier of I)

rng K186( the carrier of I, the Sorts of S) is set

Result (A,S) is Element of rng the Sorts of S

rng the Sorts of S is non empty set

K11((Args (A,S)),(Result (A,S))) is Relation-like set

K10(K11((Args (A,S)),(Result (A,S)))) is non empty set

(Den (A,S)) . {} is set

I is non empty non void V68() ManySortedSign

the carrier' of I is non empty set

S is MSAlgebra over I

A is Element of the carrier' of I

the_arity_of A is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

the carrier of I is non empty set

K183( the carrier of I) is M10( the carrier of I)

Result (A,S) is Element of rng the Sorts of S

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

rng the Sorts of S is non empty set

(I,S,A) is set

Den (A,S) is Relation-like Args (A,S) -defined Result (A,S) -valued Function-like quasi_total Element of K10(K11((Args (A,S)),(Result (A,S))))

Args (A,S) is Element of rng K186( the carrier of I, the Sorts of S)

K186( the carrier of I, the Sorts of S) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of S) is set

K11((Args (A,S)),(Result (A,S))) is Relation-like set

K10(K11((Args (A,S)),(Result (A,S)))) is non empty set

(Den (A,S)) . {} is set

dom (Den (A,S)) is Element of K10((Args (A,S)))

K10((Args (A,S))) is non empty set

rng (Den (A,S)) is Element of K10((Result (A,S)))

K10((Result (A,S))) is non empty set

I is non empty non void V68() ManySortedSign

the carrier of I is non empty set

the carrier' of I is non empty set

S is MSAlgebra over I

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

A is Element of the carrier of I

the Sorts of S . A is set

Constants (S,A) is Element of K10(( the Sorts of S . A))

K10(( the Sorts of S . A)) is non empty set

{ (I,S,b

EqR is set

K183( the carrier of I) is M10( the carrier of I)

the Arity of I is Relation-like the carrier' of I -defined K183( the carrier of I) -valued Function-like quasi_total Element of K10(K11( the carrier' of I,K183( the carrier of I)))

K11( the carrier' of I,K183( the carrier of I)) is Relation-like set

K10(K11( the carrier' of I,K183( the carrier of I))) is non empty set

the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like quasi_total Element of K10(K11( the carrier' of I, the carrier of I))

K11( the carrier' of I, the carrier of I) is non empty Relation-like set

K10(K11( the carrier' of I, the carrier of I)) is non empty set

U1 is non empty set

{ b

( the Arity of I . b

U1 is non empty set

{ b

( the Arity of I . b

U2 is Element of U1

U19 is Element of the carrier' of I

the Arity of I . U19 is Element of K183( the carrier of I)

the ResultSort of I . U19 is Element of the carrier of I

Result (U19,S) is Element of rng the Sorts of S

rng the Sorts of S is non empty set

Den (U19,S) is Relation-like Args (U19,S) -defined Result (U19,S) -valued Function-like quasi_total Element of K10(K11((Args (U19,S)),(Result (U19,S))))

Args (U19,S) is Element of rng K186( the carrier of I, the Sorts of S)

K186( the carrier of I, the Sorts of S) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of S) is set

K11((Args (U19,S)),(Result (U19,S))) is Relation-like set

K10(K11((Args (U19,S)),(Result (U19,S)))) is non empty set

rng (Den (U19,S)) is Element of K10((Result (U19,S)))

K10((Result (U19,S))) is non empty set

U19 is Element of the carrier' of I

the Arity of I . U19 is Element of K183( the carrier of I)

the ResultSort of I . U19 is Element of the carrier of I

Result (U19,S) is Element of rng the Sorts of S

rng the Sorts of S is non empty set

Den (U19,S) is Relation-like Args (U19,S) -defined Result (U19,S) -valued Function-like quasi_total Element of K10(K11((Args (U19,S)),(Result (U19,S))))

Args (U19,S) is Element of rng K186( the carrier of I, the Sorts of S)

K186( the carrier of I, the Sorts of S) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of S) is set

K11((Args (U19,S)),(Result (U19,S))) is Relation-like set

K10(K11((Args (U19,S)),(Result (U19,S)))) is non empty set

rng (Den (U19,S)) is Element of K10((Result (U19,S)))

K10((Result (U19,S))) is non empty set

dom (Den (U19,S)) is Element of K10((Args (U19,S)))

K10((Args (U19,S))) is non empty set

the_result_sort_of U19 is Element of the carrier of I

the_arity_of U19 is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

(I,S,U19) is set

(Den (U19,S)) . {} is set

U29 is set

(Den (U19,S)) . U29 is set

EqR is set

U1 is Element of the carrier' of I

(I,S,U1) is set

Den (U1,S) is Relation-like Args (U1,S) -defined Result (U1,S) -valued Function-like quasi_total Element of K10(K11((Args (U1,S)),(Result (U1,S))))

Args (U1,S) is Element of rng K186( the carrier of I, the Sorts of S)

K186( the carrier of I, the Sorts of S) is Relation-like K183( the carrier of I) -defined Function-like total set

K183( the carrier of I) is M10( the carrier of I)

rng K186( the carrier of I, the Sorts of S) is set

Result (U1,S) is Element of rng the Sorts of S

rng the Sorts of S is non empty set

K11((Args (U1,S)),(Result (U1,S))) is Relation-like set

K10(K11((Args (U1,S)),(Result (U1,S)))) is non empty set

(Den (U1,S)) . {} is set

the_result_sort_of U1 is Element of the carrier of I

the_arity_of U1 is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like quasi_total Element of K10(K11( the carrier' of I, the carrier of I))

K11( the carrier' of I, the carrier of I) is non empty Relation-like set

K10(K11( the carrier' of I, the carrier of I)) is non empty set

dom the ResultSort of I is Element of K10( the carrier' of I)

K10( the carrier' of I) is non empty set

the ResultSort of I * the Sorts of S is non empty Relation-like the carrier' of I -defined Function-like total set

( the ResultSort of I * the Sorts of S) . U1 is set

the ResultSort of I . U1 is Element of the carrier of I

the Sorts of S . ( the ResultSort of I . U1) is set

the Arity of I is Relation-like the carrier' of I -defined K183( the carrier of I) -valued Function-like quasi_total Element of K10(K11( the carrier' of I,K183( the carrier of I)))

K11( the carrier' of I,K183( the carrier of I)) is Relation-like set

K10(K11( the carrier' of I,K183( the carrier of I))) is non empty set

the Arity of I . U1 is Element of K183( the carrier of I)

rng (Den (U1,S)) is Element of K10((Result (U1,S)))

K10((Result (U1,S))) is non empty set

dom (Den (U1,S)) is Element of K10((Args (U1,S)))

K10((Args (U1,S))) is non empty set

U2 is non empty set

{ b

( the Arity of I . b

U19 is Element of the carrier' of I

the Arity of I . U19 is Element of K183( the carrier of I)

the ResultSort of I . U19 is Element of the carrier of I

Result (U19,S) is Element of rng the Sorts of S

Den (U19,S) is Relation-like Args (U19,S) -defined Result (U19,S) -valued Function-like quasi_total Element of K10(K11((Args (U19,S)),(Result (U19,S))))

Args (U19,S) is Element of rng K186( the carrier of I, the Sorts of S)

K11((Args (U19,S)),(Result (U19,S))) is Relation-like set

K10(K11((Args (U19,S)),(Result (U19,S)))) is non empty set

rng (Den (U19,S)) is Element of K10((Result (U19,S)))

K10((Result (U19,S))) is non empty set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

OPER A is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (OPER A) is Relation-like Function-like Function-yielding V54() set

EqR is Element of the carrier' of S

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

the carrier of S is non empty set

K183( the carrier of S) is M10( the carrier of S)

(commute (OPER A)) . EqR is Relation-like Function-like set

{ (Result (EqR,(A . b

union { (Result (EqR,(A . b

Funcs ({{}},(union { (Result (EqR,(A . b

Funcs (I,(Funcs ({{}},(union { (Result (EqR,(A . b

uncurry (OPER A) is Relation-like Function-like set

rng (uncurry (OPER A)) is set

Funcs (I,(rng (uncurry (OPER A)))) is set

Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) is set

rng (commute (OPER A)) is set

U19 is Relation-like Function-like set

dom U19 is set

rng U19 is set

U19 is Relation-like Function-like set

dom U19 is set

rng U19 is set

U19 is set

rng ((commute (OPER A)) . EqR) is set

dom ((commute (OPER A)) . EqR) is set

U29 is set

((commute (OPER A)) . EqR) . U29 is set

A ?. EqR is non empty Relation-like I -defined Function-like total Function-yielding V54() set

s9 is Relation-like Function-like set

dom s9 is set

rng s9 is set

F is Relation-like Function-like set

s is Element of I

(A ?. EqR) . s is Relation-like Function-like set

A . s is non-empty MSAlgebra over S

Den (EqR,(A . s)) is Relation-like Args (EqR,(A . s)) -defined Result (EqR,(A . s)) -valued Function-like quasi_total Element of K10(K11((Args (EqR,(A . s))),(Result (EqR,(A . s)))))

Args (EqR,(A . s)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . s))

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

K186( the carrier of S, the Sorts of (A . s)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (A . s)) is set

Result (EqR,(A . s)) is non empty Element of rng the Sorts of (A . s)

rng the Sorts of (A . s) is non empty with_non-empty_elements non empty-membered set

K11((Args (EqR,(A . s))),(Result (EqR,(A . s)))) is non empty Relation-like set

K10(K11((Args (EqR,(A . s))),(Result (EqR,(A . s))))) is non empty set

dom F is set

s9 is set

rng F is set

f is set

F . f is set

(S,(A . s),EqR) is set

(Den (EqR,(A . s))) . {} is set

U19 is Relation-like Function-like set

dom U19 is set

rng U19 is set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of the carrier' of S

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

(S,(product A),EqR) is set

Den (EqR,(product A)) is Relation-like Args (EqR,(product A)) -defined Result (EqR,(product A)) -valued Function-like quasi_total Element of K10(K11((Args (EqR,(product A))),(Result (EqR,(product A)))))

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

Result (EqR,(product A)) is non empty Element of rng the Sorts of (product A)

rng the Sorts of (product A) is non empty with_non-empty_elements non empty-membered set

K11((Args (EqR,(product A))),(Result (EqR,(product A)))) is non empty Relation-like set

K10(K11((Args (EqR,(product A))),(Result (EqR,(product A))))) is non empty set

(Den (EqR,(product A))) . {} is set

{ (Result (EqR,(A . b

union { (Result (EqR,(A . b

Funcs (I,(union { (Result (EqR,(A . b

OPER A is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (OPER A) is Relation-like Function-like Function-yielding V54() set

(commute (OPER A)) . EqR is Relation-like Function-like set

Funcs ({{}},(union { (Result (EqR,(A . b

Funcs (I,(Funcs ({{}},(union { (Result (EqR,(A . b

(OPS A) . EqR is set

A ?. EqR is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (A ?. EqR) is Relation-like Function-like Function-yielding V54() set

Frege (A ?. EqR) is Relation-like product (doms (A ?. EqR)) -defined Function-like total Function-yielding V54() set

doms (A ?. EqR) is Relation-like Function-like set

product (doms (A ?. EqR)) is functional with_common_domain product-like set

Commute (Frege (A ?. EqR)) is Relation-like Function-like set

IFEQ ((the_arity_of EqR),{},(commute (A ?. EqR)),(Commute (Frege (A ?. EqR)))) is set

U19 is Relation-like Function-like set

commute U19 is Relation-like Function-like Function-yielding V54() set

(commute U19) . {} is Relation-like Function-like set

Funcs ({{}},(Funcs (I,(union { (Result (EqR,(A . b

U29 is Relation-like Function-like set

dom U29 is set

rng U29 is set

U29 . {} is set

I is non empty non void V68() ManySortedSign

the carrier' of I is non empty set

S is non empty set

EqR is non empty Relation-like S -defined Function-like total MSAlgebra-Family of S,I

product EqR is strict non-empty MSAlgebra over I

SORTS EqR is non empty Relation-like non-empty non empty-yielding the carrier of I -defined Function-like total set

the carrier of I is non empty set

OPS EqR is non empty Relation-like the carrier' of I -defined Function-like total ManySortedFunction of the Arity of I * K186( the carrier of I,(SORTS EqR)), the ResultSort of I * (SORTS EqR)

the Arity of I is Relation-like the carrier' of I -defined K183( the carrier of I) -valued Function-like quasi_total Element of K10(K11( the carrier' of I,K183( the carrier of I)))

K183( the carrier of I) is M10( the carrier of I)

K11( the carrier' of I,K183( the carrier of I)) is Relation-like set

K10(K11( the carrier' of I,K183( the carrier of I))) is non empty set

K186( the carrier of I,(SORTS EqR)) is Relation-like K183( the carrier of I) -defined Function-like total set

the Arity of I * K186( the carrier of I,(SORTS EqR)) is Relation-like the carrier' of I -defined Function-like set

the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like quasi_total Element of K10(K11( the carrier' of I, the carrier of I))

K11( the carrier' of I, the carrier of I) is non empty Relation-like set

K10(K11( the carrier' of I, the carrier of I)) is non empty set

the ResultSort of I * (SORTS EqR) is non empty Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like total set

MSAlgebra(# (SORTS EqR),(OPS EqR) #) is strict MSAlgebra over I

A is Element of the carrier' of I

(I,(product EqR),A) is set

Den (A,(product EqR)) is Relation-like Args (A,(product EqR)) -defined Result (A,(product EqR)) -valued Function-like quasi_total Element of K10(K11((Args (A,(product EqR))),(Result (A,(product EqR)))))

Args (A,(product EqR)) is non empty functional Element of rng K186( the carrier of I, the Sorts of (product EqR))

the Sorts of (product EqR) is non empty Relation-like non-empty non empty-yielding the carrier of I -defined Function-like total set

K186( the carrier of I, the Sorts of (product EqR)) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of (product EqR)) is set

Result (A,(product EqR)) is non empty Element of rng the Sorts of (product EqR)

rng the Sorts of (product EqR) is non empty with_non-empty_elements non empty-membered set

K11((Args (A,(product EqR))),(Result (A,(product EqR)))) is non empty Relation-like set

K10(K11((Args (A,(product EqR))),(Result (A,(product EqR))))) is non empty set

(Den (A,(product EqR))) . {} is set

the_arity_of A is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

{ (Result (A,(EqR . b

union { (Result (A,(EqR . b

Funcs (S,(union { (Result (A,(EqR . b

U1 is Relation-like Function-like set

dom U1 is set

rng U1 is set

the_arity_of A is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

(the_arity_of A) * the Sorts of (product EqR) is Relation-like non-empty K160() -defined Function-like set

dom ((the_arity_of A) * the Sorts of (product EqR)) is countable Element of K10(K160())

dom (the_arity_of A) is countable Element of K10(K160())

dom {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() set

dom (Den (A,(product EqR))) is functional Element of K10((Args (A,(product EqR))))

K10((Args (A,(product EqR)))) is non empty set

product ((the_arity_of A) * the Sorts of (product EqR)) is non empty functional with_common_domain product-like set

the_arity_of A is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

A is Element of I

EqR is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S

product EqR is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS EqR is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS EqR)), the ResultSort of S * (SORTS EqR)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS EqR)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS EqR)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS EqR) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS EqR),(OPS EqR) #) is strict MSAlgebra over S

EqR . A is non-empty MSAlgebra over S

U1 is Element of the carrier' of S

the_arity_of U1 is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

(S,(product EqR),U1) is Relation-like Function-like set

Den (U1,(product EqR)) is Relation-like Args (U1,(product EqR)) -defined Result (U1,(product EqR)) -valued Function-like quasi_total Element of K10(K11((Args (U1,(product EqR))),(Result (U1,(product EqR)))))

Args (U1,(product EqR)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product EqR))

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

K186( the carrier of S, the Sorts of (product EqR)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product EqR)) is set

Result (U1,(product EqR)) is non empty Element of rng the Sorts of (product EqR)

rng the Sorts of (product EqR) is non empty with_non-empty_elements non empty-membered set

K11((Args (U1,(product EqR))),(Result (U1,(product EqR)))) is non empty Relation-like set

K10(K11((Args (U1,(product EqR))),(Result (U1,(product EqR))))) is non empty set

(Den (U1,(product EqR))) . {} is set

(S,(product EqR),U1) . A is set

(S,(EqR . A),U1) is set

Den (U1,(EqR . A)) is Relation-like Args (U1,(EqR . A)) -defined Result (U1,(EqR . A)) -valued Function-like quasi_total Element of K10(K11((Args (U1,(EqR . A))),(Result (U1,(EqR . A)))))

Args (U1,(EqR . A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (EqR . A))

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

K186( the carrier of S, the Sorts of (EqR . A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (EqR . A)) is set

Result (U1,(EqR . A)) is non empty Element of rng the Sorts of (EqR . A)

rng the Sorts of (EqR . A) is non empty with_non-empty_elements non empty-membered set

K11((Args (U1,(EqR . A))),(Result (U1,(EqR . A)))) is non empty Relation-like set

K10(K11((Args (U1,(EqR . A))),(Result (U1,(EqR . A))))) is non empty set

(Den (U1,(EqR . A))) . {} is set

OPER EqR is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (OPER EqR) is Relation-like Function-like Function-yielding V54() set

(commute (OPER EqR)) . U1 is Relation-like Function-like set

{ (Result (U1,(EqR . b

union { (Result (U1,(EqR . b

Funcs ({{}},(union { (Result (U1,(EqR . b

Funcs (I,(Funcs ({{}},(union { (Result (U1,(EqR . b

(OPS EqR) . U1 is set

EqR ?. U1 is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (EqR ?. U1) is Relation-like Function-like Function-yielding V54() set

Frege (EqR ?. U1) is Relation-like product (doms (EqR ?. U1)) -defined Function-like total Function-yielding V54() set

doms (EqR ?. U1) is Relation-like Function-like set

product (doms (EqR ?. U1)) is functional with_common_domain product-like set

Commute (Frege (EqR ?. U1)) is Relation-like Function-like set

IFEQ ((the_arity_of U1),{},(commute (EqR ?. U1)),(Commute (Frege (EqR ?. U1)))) is set

commute ((commute (OPER EqR)) . U1) is Relation-like Function-like Function-yielding V54() set

(commute ((commute (OPER EqR)) . U1)) . {} is Relation-like Function-like set

(EqR ?. U1) . A is Relation-like Function-like set

((EqR ?. U1) . A) . {} is set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of the carrier' of S

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

(S,(product A),EqR) is Relation-like Function-like set

Den (EqR,(product A)) is Relation-like Args (EqR,(product A)) -defined Result (EqR,(product A)) -valued Function-like quasi_total Element of K10(K11((Args (EqR,(product A))),(Result (EqR,(product A)))))

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

Result (EqR,(product A)) is non empty Element of rng the Sorts of (product A)

rng the Sorts of (product A) is non empty with_non-empty_elements non empty-membered set

K11((Args (EqR,(product A))),(Result (EqR,(product A)))) is non empty Relation-like set

K10(K11((Args (EqR,(product A))),(Result (EqR,(product A))))) is non empty set

(Den (EqR,(product A))) . {} is set

U1 is Relation-like Function-like set

dom U1 is set

U2 is set

U1 . U2 is set

U19 is Element of I

A . U19 is non-empty MSAlgebra over S

(S,(A . U19),EqR) is set

Den (EqR,(A . U19)) is Relation-like Args (EqR,(A . U19)) -defined Result (EqR,(A . U19)) -valued Function-like quasi_total Element of K10(K11((Args (EqR,(A . U19))),(Result (EqR,(A . U19)))))

Args (EqR,(A . U19)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . U19))

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

K186( the carrier of S, the Sorts of (A . U19)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (A . U19)) is set

Result (EqR,(A . U19)) is non empty Element of rng the Sorts of (A . U19)

rng the Sorts of (A . U19) is non empty with_non-empty_elements non empty-membered set

K11((Args (EqR,(A . U19))),(Result (EqR,(A . U19)))) is non empty Relation-like set

K10(K11((Args (EqR,(A . U19))),(Result (EqR,(A . U19))))) is non empty set

(Den (EqR,(A . U19))) . {} is set

(S,(product A),EqR) . U2 is set

{ (Result (EqR,(A . b

union { (Result (EqR,(A . b

Funcs (I,(union { (Result (EqR,(A . b

U19 is Relation-like Function-like set

dom U19 is set

rng U19 is set

I is non empty non void V68() ManySortedSign

the carrier' of I is non empty set

the carrier of I is non empty set

S is MSAlgebra over I

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

A is MSAlgebra over I

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

EqR is Element of the carrier' of I

Args (EqR,S) is Element of rng K186( the carrier of I, the Sorts of S)

K186( the carrier of I, the Sorts of S) is Relation-like K183( the carrier of I) -defined Function-like total set

K183( the carrier of I) is M10( the carrier of I)

rng K186( the carrier of I, the Sorts of S) is set

the_arity_of EqR is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

Args (EqR,A) is Element of rng K186( the carrier of I, the Sorts of A)

K186( the carrier of I, the Sorts of A) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of A) is set

U1 is Element of Args (EqR,S)

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

U19 # U1 is Element of Args (EqR,A)

rng (the_arity_of EqR) is Element of K10( the carrier of I)

K10( the carrier of I) is non empty set

dom U19 is non empty Element of K10( the carrier of I)

(the_arity_of EqR) * U19 is Relation-like K160() -defined Function-like Function-yielding V54() set

dom ((the_arity_of EqR) * U19) is countable Element of K10(K160())

dom (the_arity_of EqR) is countable Element of K10(K160())

rng ((the_arity_of EqR) * U19) is set

K11({},{}) is Relation-like set

K10(K11({},{})) is non empty set

U2 is Relation-like Function-like set

doms ((the_arity_of EqR) * U19) is Relation-like Function-like set

product (doms ((the_arity_of EqR) * U19)) is functional with_common_domain product-like set

Frege ((the_arity_of EqR) * U19) is Relation-like product (doms ((the_arity_of EqR) * U19)) -defined Function-like total Function-yielding V54() set

(Frege ((the_arity_of EqR) * U19)) . U1 is Relation-like Function-like set

((the_arity_of EqR) * U19) .. U2 is Relation-like Function-like set

U29 is Relation-like Function-like set

dom U29 is set

I is non empty non void V68() ManySortedSign

the carrier' of I is non empty set

the carrier of I is non empty set

S is Element of the carrier' of I

the_arity_of S is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

K183( the carrier of I) is M10( the carrier of I)

A is non-empty MSAlgebra over I

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

EqR is non-empty MSAlgebra over I

the Sorts of EqR is non empty Relation-like non-empty non empty-yielding the carrier of I -defined Function-like total set

Args (S,A) is non empty functional Element of rng K186( the carrier of I, the Sorts of A)

K186( the carrier of I, the Sorts of A) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of A) is set

U1 is non empty Relation-like the carrier of I -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of A, the Sorts of EqR

(the_arity_of S) * U1 is Relation-like K160() -defined Function-like Function-yielding V54() set

doms ((the_arity_of S) * U1) is Relation-like Function-like set

product (doms ((the_arity_of S) * U1)) is functional with_common_domain product-like set

U2 is Relation-like Function-like Element of Args (S,A)

(the_arity_of S) * the Sorts of A is Relation-like non-empty K160() -defined Function-like set

product ((the_arity_of S) * the Sorts of A) is non empty functional with_common_domain product-like set

dom U2 is set

dom ((the_arity_of S) * the Sorts of A) is countable Element of K10(K160())

dom (the_arity_of S) is countable Element of K10(K160())

dom U1 is non empty Element of K10( the carrier of I)

K10( the carrier of I) is non empty set

rng (the_arity_of S) is Element of K10( the carrier of I)

U19 is set

dom (doms ((the_arity_of S) * U1)) is set

rng ((the_arity_of S) * U1) is set

SubFuncs (rng ((the_arity_of S) * U1)) is set

((the_arity_of S) * U1) " (SubFuncs (rng ((the_arity_of S) * U1))) is set

dom ((the_arity_of S) * U1) is countable Element of K10(K160())

U19 is set

(the_arity_of S) . U19 is set

((the_arity_of S) * U1) . U19 is Relation-like Function-like set

U29 is Element of the carrier of I

U1 . U29 is Relation-like the Sorts of A . U29 -defined the Sorts of EqR . U29 -valued Function-like quasi_total Element of K10(K11(( the Sorts of A . U29),( the Sorts of EqR . U29)))

the Sorts of A . U29 is non empty set

the Sorts of EqR . U29 is non empty set

K11(( the Sorts of A . U29),( the Sorts of EqR . U29)) is non empty Relation-like set

K10(K11(( the Sorts of A . U29),( the Sorts of EqR . U29))) is non empty set

(doms ((the_arity_of S) * U1)) . U19 is set

dom (U1 . U29) is Element of K10(( the Sorts of A . U29))

K10(( the Sorts of A . U29)) is non empty set

U2 . U19 is set

((the_arity_of S) * the Sorts of A) . U19 is set

U19 is set

((the_arity_of S) * U1) . U19 is Relation-like Function-like set

I is non empty non void V68() ManySortedSign

the carrier' of I is non empty set

the carrier of I is non empty set

S is Element of the carrier' of I

the_arity_of S is Relation-like K160() -defined the carrier of I -valued Function-like V70() M11( the carrier of I,K183( the carrier of I))

K183( the carrier of I) is M10( the carrier of I)

dom (the_arity_of S) is countable Element of K10(K160())

A is non-empty MSAlgebra over I

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

EqR is non-empty MSAlgebra over I

the Sorts of EqR is non empty Relation-like non-empty non empty-yielding the carrier of I -defined Function-like total set

Args (S,A) is non empty functional Element of rng K186( the carrier of I, the Sorts of A)

K186( the carrier of I, the Sorts of A) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of A) is set

U1 is non empty Relation-like the carrier of I -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of A, the Sorts of EqR

U2 is Relation-like Function-like Element of Args (S,A)

U1 # U2 is Relation-like Function-like Element of Args (S,EqR)

Args (S,EqR) is non empty functional Element of rng K186( the carrier of I, the Sorts of EqR)

K186( the carrier of I, the Sorts of EqR) is Relation-like K183( the carrier of I) -defined Function-like total set

rng K186( the carrier of I, the Sorts of EqR) is set

U19 is set

(U1 # U2) . U19 is set

(the_arity_of S) /. U19 is Element of the carrier of I

U1 . ((the_arity_of S) /. U19) is Relation-like the Sorts of A . ((the_arity_of S) /. U19) -defined the Sorts of EqR . ((the_arity_of S) /. U19) -valued Function-like quasi_total Element of K10(K11(( the Sorts of A . ((the_arity_of S) /. U19)),( the Sorts of EqR . ((the_arity_of S) /. U19))))

the Sorts of A . ((the_arity_of S) /. U19) is non empty set

the Sorts of EqR . ((the_arity_of S) /. U19) is non empty set

K11(( the Sorts of A . ((the_arity_of S) /. U19)),( the Sorts of EqR . ((the_arity_of S) /. U19))) is non empty Relation-like set

K10(K11(( the Sorts of A . ((the_arity_of S) /. U19)),( the Sorts of EqR . ((the_arity_of S) /. U19)))) is non empty set

U2 . U19 is set

(U1 . ((the_arity_of S) /. U19)) . (U2 . U19) is set

dom U1 is non empty Element of K10( the carrier of I)

K10( the carrier of I) is non empty set

rng (the_arity_of S) is Element of K10( the carrier of I)

(the_arity_of S) * U1 is Relation-like K160() -defined Function-like Function-yielding V54() set

dom ((the_arity_of S) * U1) is countable Element of K10(K160())

doms ((the_arity_of S) * U1) is Relation-like Function-like set

product (doms ((the_arity_of S) * U1)) is functional with_common_domain product-like set

Frege ((the_arity_of S) * U1) is Relation-like product (doms ((the_arity_of S) * U1)) -defined Function-like total Function-yielding V54() set

(Frege ((the_arity_of S) * U1)) . U2 is Relation-like Function-like set

((Frege ((the_arity_of S) * U1)) . U2) . U19 is set

((the_arity_of S) * U1) .. U2 is Relation-like Function-like set

(((the_arity_of S) * U1) .. U2) . U19 is set

((the_arity_of S) * U1) . U19 is Relation-like Function-like set

(((the_arity_of S) * U1) . U19) . (U2 . U19) is set

(the_arity_of S) . U19 is set

U1 . ((the_arity_of S) . U19) is Relation-like Function-like set

(U1 . ((the_arity_of S) . U19)) . (U2 . U19) is set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

{ ( the Sorts of (A . b

union { ( the Sorts of (A . b

Funcs (I,(union { ( the Sorts of (A . b

EqR is Element of the carrier' of S

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

dom (the_arity_of EqR) is countable Element of K10(K160())

Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b

U1 is Relation-like Function-like Element of Args (EqR,(product A))

U19 is Relation-like Function-like set

(the_arity_of EqR) * the Sorts of (product A) is Relation-like non-empty K160() -defined Function-like set

product ((the_arity_of EqR) * the Sorts of (product A)) is non empty functional with_common_domain product-like set

dom (SORTS A) is non empty Element of K10( the carrier of S)

K10( the carrier of S) is non empty set

rng (the_arity_of EqR) is Element of K10( the carrier of S)

U29 is set

rng U19 is set

dom U19 is set

F is set

U19 . F is set

(the_arity_of EqR) * (SORTS A) is Relation-like non-empty K160() -defined Function-like set

dom ((the_arity_of EqR) * (SORTS A)) is countable Element of K10(K160())

(the_arity_of EqR) . F is set

((the_arity_of EqR) * (SORTS A)) . F is set

s is Element of the carrier of S

(SORTS A) . s is non empty set

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

product (Carrier (A,s)) is non empty functional with_common_domain product-like set

dom (Carrier (A,s)) is non empty Element of K10(I)

K10(I) is non empty set

s9 is Relation-like Function-like set

dom s9 is set

f is set

rng s9 is set

y is set

s9 . y is set

x is Element of I

A . x is non-empty MSAlgebra over S

(Carrier (A,s)) . x is non empty set

s9 . x is set

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

the Sorts of (A . x) . s is non empty set

x is MSAlgebra over S

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

the Sorts of x . s is set

dom U1 is set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of the carrier' of S

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

dom (the_arity_of EqR) is countable Element of K10(K160())

U1 is Relation-like Function-like Element of Args (EqR,(product A))

U2 is set

U1 . U2 is set

(the_arity_of EqR) /. U2 is Element of the carrier of S

Carrier (A,((the_arity_of EqR) /. U2)) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set

product (Carrier (A,((the_arity_of EqR) /. U2))) is non empty functional with_common_domain product-like set

dom (SORTS A) is non empty Element of K10( the carrier of S)

K10( the carrier of S) is non empty set

rng (the_arity_of EqR) is Element of K10( the carrier of S)

(the_arity_of EqR) * (SORTS A) is Relation-like non-empty K160() -defined Function-like set

dom ((the_arity_of EqR) * (SORTS A)) is countable Element of K10(K160())

(the_arity_of EqR) * the Sorts of (product A) is Relation-like non-empty K160() -defined Function-like set

product ((the_arity_of EqR) * the Sorts of (product A)) is non empty functional with_common_domain product-like set

((the_arity_of EqR) * (SORTS A)) . U2 is set

(the_arity_of EqR) . U2 is set

(SORTS A) . ((the_arity_of EqR) . U2) is set

(SORTS A) . ((the_arity_of EqR) /. U2) is non empty set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of the carrier' of S

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

dom (the_arity_of EqR) is countable Element of K10(K160())

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

U1 is Element of I

A . U1 is non-empty MSAlgebra over S

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

U2 is set

(the_arity_of EqR) . U2 is set

(the_arity_of EqR) * the Sorts of (product A) is Relation-like non-empty K160() -defined Function-like set

dom ((the_arity_of EqR) * the Sorts of (product A)) is countable Element of K10(K160())

U19 is Element of the carrier of S

the Sorts of (A . U1) . U19 is non empty set

U29 is Relation-like Function-like Element of Args (EqR,(product A))

U29 . U2 is set

product ((the_arity_of EqR) * the Sorts of (product A)) is non empty functional with_common_domain product-like set

F is Relation-like Function-like set

F . U1 is set

((the_arity_of EqR) * the Sorts of (product A)) . U2 is set

the Sorts of (product A) . U19 is non empty set

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

product (Carrier (A,U19)) is non empty functional with_common_domain product-like set

dom (Carrier (A,U19)) is non empty Element of K10(I)

K10(I) is non empty set

(Carrier (A,U19)) . U1 is non empty set

s is MSAlgebra over S

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

the Sorts of s . U19 is set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of the carrier' of S

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

A ?. EqR is non empty Relation-like I -defined Function-like total Function-yielding V54() set

OPER A is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (OPER A) is Relation-like Function-like Function-yielding V54() set

(commute (OPER A)) . EqR is Relation-like Function-like set

doms (A ?. EqR) is Relation-like Function-like set

product (doms (A ?. EqR)) is functional with_common_domain product-like set

U1 is Relation-like Function-like Element of Args (EqR,(product A))

commute U1 is Relation-like Function-like Function-yielding V54() set

{ ( the Sorts of (A . b

union { ( the Sorts of (A . b

dom (the_arity_of EqR) is countable Element of K10(K160())

Funcs (I,(union { ( the Sorts of (A . b

Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b

Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b

Funcs (I,(Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b

U19 is set

dom (doms (A ?. EqR)) is set

F is set

U29 is Element of I

A . U29 is non-empty MSAlgebra over S

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

(the_arity_of EqR) * the Sorts of (A . U29) is Relation-like non-empty K160() -defined Function-like set

dom ((the_arity_of EqR) * the Sorts of (A . U29)) is countable Element of K10(K160())

(the_arity_of EqR) . F is set

rng (the_arity_of EqR) is Element of K10( the carrier of S)

K10( the carrier of S) is non empty set

dom U1 is set

s9 is Relation-like Function-like set

dom s9 is set

rng s9 is set

U1 . F is set

rng U1 is set

s9 is Relation-like Function-like set

dom s9 is set

rng s9 is set

s9 is Relation-like Function-like set

dom s9 is set

rng s9 is set

(commute U1) . U29 is Relation-like Function-like set

((commute U1) . U29) . F is set

s9 . U29 is set

s is Element of the carrier of S

the Sorts of (A . U29) . s is non empty set

((the_arity_of EqR) * the Sorts of (A . U29)) . F is set

rng (commute U1) is set

F is Relation-like Function-like set

dom F is set

rng F is set

F is Relation-like Function-like set

dom F is set

rng F is set

dom ((commute U1) . U29) is set

F is Relation-like Function-like set

dom F is set

rng F is set

product ((the_arity_of EqR) * the Sorts of (A . U29)) is non empty functional with_common_domain product-like set

Args (EqR,(A . U29)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . U29))

K186( the carrier of S, the Sorts of (A . U29)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (A . U29)) is set

(commute U1) . U19 is Relation-like Function-like set

(doms (A ?. EqR)) . U19 is set

dom (commute U1) is set

U19 is Relation-like Function-like set

dom U19 is set

rng U19 is set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of the carrier' of S

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

the_arity_of EqR is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

A ?. EqR is non empty Relation-like I -defined Function-like total Function-yielding V54() set

OPER A is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (OPER A) is Relation-like Function-like Function-yielding V54() set

(commute (OPER A)) . EqR is Relation-like Function-like set

Frege (A ?. EqR) is Relation-like product (doms (A ?. EqR)) -defined Function-like total Function-yielding V54() set

doms (A ?. EqR) is Relation-like Function-like set

product (doms (A ?. EqR)) is functional with_common_domain product-like set

Commute (Frege (A ?. EqR)) is Relation-like Function-like set

dom (Commute (Frege (A ?. EqR))) is set

U1 is Relation-like Function-like Element of Args (EqR,(product A))

{ ( the Sorts of (A . b

union { ( the Sorts of (A . b

commute U1 is Relation-like Function-like Function-yielding V54() set

dom (Frege (A ?. EqR)) is functional with_common_domain Element of K10((product (doms (A ?. EqR))))

K10((product (doms (A ?. EqR)))) is non empty set

dom (the_arity_of EqR) is countable Element of K10(K160())

Funcs (I,(union { ( the Sorts of (A . b

Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b

commute (commute U1) is Relation-like Function-like Function-yielding V54() set

I is set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of the carrier' of S

Args (EqR,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

Result (EqR,(product A)) is non empty Element of rng the Sorts of (product A)

rng the Sorts of (product A) is non empty with_non-empty_elements non empty-membered set

Den (EqR,(product A)) is Relation-like Args (EqR,(product A)) -defined Result (EqR,(product A)) -valued Function-like quasi_total Element of K10(K11((Args (EqR,(product A))),(Result (EqR,(product A)))))

K11((Args (EqR,(product A))),(Result (EqR,(product A)))) is non empty Relation-like set

K10(K11((Args (EqR,(product A))),(Result (EqR,(product A))))) is non empty set

the_result_sort_of EqR is Element of the carrier of S

Carrier (A,(the_result_sort_of EqR)) is Relation-like non-empty I -defined Function-like total set

product (Carrier (A,(the_result_sort_of EqR))) is non empty functional with_common_domain product-like set

U1 is Relation-like Function-like Element of Args (EqR,(product A))

(Den (EqR,(product A))) . U1 is Element of Result (EqR,(product A))

(SORTS A) . (the_result_sort_of EqR) is non empty set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like total ManySortedFunction of the Arity of S * K186( the carrier of S,(SORTS A)), the ResultSort of S * (SORTS A)

the Arity of S is Relation-like the carrier' of S -defined K183( the carrier of S) -valued Function-like quasi_total Element of K10(K11( the carrier' of S,K183( the carrier of S)))

K183( the carrier of S) is M10( the carrier of S)

K11( the carrier' of S,K183( the carrier of S)) is Relation-like set

K10(K11( the carrier' of S,K183( the carrier of S))) is non empty set

K186( the carrier of S,(SORTS A)) is Relation-like K183( the carrier of S) -defined Function-like total set

the Arity of S * K186( the carrier of S,(SORTS A)) is Relation-like the carrier' of S -defined Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of K10(K11( the carrier' of S, the carrier of S))

K11( the carrier' of S, the carrier of S) is non empty Relation-like set

K10(K11( the carrier' of S, the carrier of S)) is non empty set

the ResultSort of S * (SORTS A) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over S

EqR is Element of I

A . EqR is non-empty MSAlgebra over S

U1 is Element of the carrier' of S

the_arity_of U1 is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))

Args (U1,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))

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

K186( the carrier of S, the Sorts of (product A)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (product A)) is set

Args (U1,(A . EqR)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . EqR))

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

K186( the carrier of S, the Sorts of (A . EqR)) is Relation-like K183( the carrier of S) -defined Function-like total set

rng K186( the carrier of S, the Sorts of (A . EqR)) is set

U19 is Relation-like Function-like Element of Args (U1,(product A))

commute U19 is Relation-like Function-like Function-yielding V54() set

(commute U19) . EqR is Relation-like Function-like set

A ?. U1 is non empty Relation-like I -defined Function-like total Function-yielding V54() set

OPER A is non empty Relation-like I -defined Function-like total Function-yielding V54() set

commute (OPER A) is Relation-like Function-like Function-yielding V54() set

(commute (OPER A)) . U1 is Relation-like Function-like set

doms (A ?. U1) is Relation-like Function-like set

dom (doms (A ?. U1)) is set

product (doms (A ?. U1)) is functional with_common_domain product-like set

(doms (A ?. U1)) . EqR is set

I is non empty set

S is non empty non void V68() ManySortedSign

the carrier' of S is non empty set

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

product A is strict non-empty MSAlgebra over S

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

the carrier of S is non empty set

OPS A is non empty Relation-like the carrier' of S -defined Function-like