:: PRALG_3 semantic presentation

K160() is V40() countable denumerable Element of K10(K156())
K156() is set
K10(K156()) is non empty set

K10(K109()) is non empty set
K10(K160()) is non empty set
K205() is 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

I is set
S is non empty non void V68() ManySortedSign

product A is strict MSAlgebra over S

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(OPS A) #) is strict MSAlgebra over S

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

A is set
S . A is set

A is 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)

(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 non empty set

rng S is non empty set

{ (rng (S . b1)) where b1 is Element of I : verum } is set
union { (rng (S . b1)) where b1 is Element of I : verum } is set
U1 is non empty functional with_common_domain set
DOM U1 is set

rng EqR is set
Funcs ((DOM U1),(union { (rng (S . b1)) where b1 is Element of I : verum } )) is set
U2 is set
dom S is non empty Element of K10(I)
K10(I) is non empty set
U19 is set

U29 is Element of I

rng F is set
s is set
dom F is set
U2 is Element of I

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

(() . U19) . U2 is set
dom EqR is set
Funcs (I,(Funcs ((DOM U1),(union { (rng (S . b1)) where b1 is Element of I : verum } )))) is set
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,b1) where b1 is Element of the carrier' of I : ( the_result_sort_of b1 = A & the_arity_of b1 = {} ) } is set
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
{ b1 where b1 is Element of U1 : ex b2 being Element of the carrier' of I st
( the Arity of I . b2 = {} & the ResultSort of I . b2 = A & b1 in rng (Den (b2,S)) )
}
is set

U1 is non empty set
{ b1 where b1 is Element of U1 : ex b2 being Element of the carrier' of I st
( the Arity of I . b2 = {} & the ResultSort of I . b2 = A & b1 in rng (Den (b2,S)) )
}
is set

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
{ b1 where b1 is Element of U2 : ex b2 being Element of the carrier' of I st
( the Arity of I . b2 = {} & the ResultSort of I . b2 = A & b1 in rng (Den (b2,S)) )
}
is 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
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

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 . b1))) where b1 is Element of I : verum } is set
union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } is set
Funcs (,(union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } )) is set
Funcs (I,(Funcs (,(union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } )))) is 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

dom U19 is set
rng U19 is 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

dom s9 is set
rng s9 is 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

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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(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,(),EqR) is set
Den (EqR,()) is Relation-like Args (EqR,()) -defined Result (EqR,()) -valued Function-like quasi_total Element of K10(K11((Args (EqR,())),(Result (EqR,()))))
Args (EqR,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) is set
Result (EqR,()) is non empty Element of rng the Sorts of ()
rng the Sorts of () is non empty with_non-empty_elements non empty-membered set
K11((Args (EqR,())),(Result (EqR,()))) is non empty Relation-like set
K10(K11((Args (EqR,())),(Result (EqR,())))) is non empty set
(Den (EqR,())) . {} is set
{ (Result (EqR,(A . b1))) where b1 is Element of I : verum } is set
union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } is set
Funcs (I,(union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } )) is set

(commute (OPER A)) . EqR is Relation-like Function-like set
Funcs (,(union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } )) is set
Funcs (I,(Funcs (,(union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } )))) is set
(OPS A) . EqR is 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

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

Funcs (,(Funcs (I,(union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } )))) is 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

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 . b1))) where b1 is Element of S : verum } is set
union { (Result (A,(EqR . b1))) where b1 is Element of S : verum } is set
Funcs (S,(union { (Result (A,(EqR . b1))) where b1 is Element of S : verum } )) is 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 Sorts of (product EqR) is Relation-like non-empty K160() -defined Function-like set
dom (() * the Sorts of (product EqR)) is countable Element of K10(K160())
dom () is countable Element of K10(K160())

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 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

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

(commute (OPER EqR)) . U1 is Relation-like Function-like set
{ (Result (U1,(EqR . b1))) where b1 is Element of I : verum } is set
union { (Result (U1,(EqR . b1))) where b1 is Element of I : verum } is set
Funcs (,(union { (Result (U1,(EqR . b1))) where b1 is Element of I : verum } )) is set
Funcs (I,(Funcs (,(union { (Result (U1,(EqR . b1))) where b1 is Element of I : verum } )))) is set
(OPS EqR) . U1 is 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 ((),{},(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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(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,(),EqR) is Relation-like Function-like set
Den (EqR,()) is Relation-like Args (EqR,()) -defined Result (EqR,()) -valued Function-like quasi_total Element of K10(K11((Args (EqR,())),(Result (EqR,()))))
Args (EqR,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) is set
Result (EqR,()) is non empty Element of rng the Sorts of ()
rng the Sorts of () is non empty with_non-empty_elements non empty-membered set
K11((Args (EqR,())),(Result (EqR,()))) is non empty Relation-like set
K10(K11((Args (EqR,())),(Result (EqR,())))) is non empty set
(Den (EqR,())) . {} is 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,(),EqR) . U2 is set
{ (Result (EqR,(A . b1))) where b1 is Element of I : verum } is set
union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } is set
Funcs (I,(union { (Result (EqR,(A . b1))) where b1 is Element of I : verum } )) is 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)

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

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

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

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

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

product (() * the Sorts of A) is non empty functional with_common_domain product-like set
dom U2 is set
dom (() * the Sorts of A) is countable Element of K10(K160())
dom () 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 () is Element of K10( the carrier of I)
U19 is set
dom (doms (() * U1)) is set
rng (() * U1) is set
SubFuncs (rng (() * U1)) is set
(() * U1) " (SubFuncs (rng (() * U1))) is set
dom (() * U1) is countable Element of K10(K160())
U19 is set
() . U19 is set
(() * 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 (() * 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 Sorts of A) . U19 is set
U19 is set
(() * 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 () 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
() /. U19 is Element of the carrier of I
U1 . (() /. U19) is Relation-like the Sorts of A . (() /. U19) -defined the Sorts of EqR . (() /. U19) -valued Function-like quasi_total Element of K10(K11(( the Sorts of A . (() /. U19)),( the Sorts of EqR . (() /. U19))))
the Sorts of A . (() /. U19) is non empty set
the Sorts of EqR . (() /. U19) is non empty set
K11(( the Sorts of A . (() /. U19)),( the Sorts of EqR . (() /. U19))) is non empty Relation-like set
K10(K11(( the Sorts of A . (() /. U19)),( the Sorts of EqR . (() /. U19)))) is non empty set
U2 . U19 is set
(U1 . (() /. 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 () is Element of K10( the carrier of I)

dom (() * U1) is countable Element of K10(K160())
doms (() * U1) is Relation-like Function-like set

Frege (() * U1) is Relation-like product (doms (() * U1)) -defined Function-like total Function-yielding V54() set
(Frege (() * U1)) . U2 is Relation-like Function-like set
((Frege (() * U1)) . U2) . U19 is set
(() * U1) .. U2 is Relation-like Function-like set
((() * U1) .. U2) . U19 is set
(() * U1) . U19 is Relation-like Function-like set
((() * U1) . U19) . (U2 . U19) is set
() . U19 is set
U1 . (() . U19) is Relation-like Function-like set
(U1 . (() . 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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(OPS A) #) is strict MSAlgebra over S
{ ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } is set
Funcs (I,(union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )) is set
EqR is Element of the carrier' of S
Args (EqR,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) 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 . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )))) is set
U1 is Relation-like Function-like Element of Args (EqR,())

(the_arity_of EqR) * the Sorts of () is Relation-like non-empty K160() -defined Function-like set
product ((the_arity_of EqR) * the Sorts of ()) is non empty functional with_common_domain product-like set
dom () 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

dom ((the_arity_of EqR) * ()) is countable Element of K10(K160())
(the_arity_of EqR) . F is set
((the_arity_of EqR) * ()) . F is set
s is Element of the carrier of S
() . s is non empty 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

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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(OPS A) #) is strict MSAlgebra over S
EqR is Element of the carrier' of S
Args (EqR,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) 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,())
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 () 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)

dom ((the_arity_of EqR) * ()) is countable Element of K10(K160())
(the_arity_of EqR) * the Sorts of () is Relation-like non-empty K160() -defined Function-like set
product ((the_arity_of EqR) * the Sorts of ()) is non empty functional with_common_domain product-like set
((the_arity_of EqR) * ()) . U2 is set
(the_arity_of EqR) . U2 is set
() . ((the_arity_of EqR) . U2) is set
() . ((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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(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,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) 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 () is Relation-like non-empty K160() -defined Function-like set
dom ((the_arity_of EqR) * the Sorts of ()) 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,())
U29 . U2 is set
product ((the_arity_of EqR) * the Sorts of ()) is non empty functional with_common_domain product-like set

F . U1 is set
((the_arity_of EqR) * the Sorts of ()) . U2 is set
the Sorts of () . 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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(OPS A) #) is strict MSAlgebra over S
EqR is Element of the carrier' of S
Args (EqR,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) 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))

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

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

{ ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } is set
dom (the_arity_of EqR) is countable Element of K10(K160())
Funcs (I,(union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )) is set
Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )))) is set
Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )))) is set
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

dom s9 is set
rng s9 is set
U1 . F is set
rng U1 is set

dom s9 is set
rng s9 is 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

dom F is set
rng F is set

dom F is set
rng F is set
dom ((commute U1) . U29) is 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

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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(OPS A) #) is strict MSAlgebra over S
EqR is Element of the carrier' of S
Args (EqR,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) 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))

(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

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,())
{ ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } is 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 . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )) is set
Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b1) . b2) where b1 is Element of I, b2 is Element of the carrier of S : verum } )))) is set

I is set
S is non empty non void V68() ManySortedSign
the carrier' of S is non empty set

product A is strict non-empty MSAlgebra over S

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(OPS A) #) is strict MSAlgebra over S
EqR is Element of the carrier' of S
Args (EqR,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) is set
Result (EqR,()) is non empty Element of rng the Sorts of ()
rng the Sorts of () is non empty with_non-empty_elements non empty-membered set
Den (EqR,()) is Relation-like Args (EqR,()) -defined Result (EqR,()) -valued Function-like quasi_total Element of K10(K11((Args (EqR,())),(Result (EqR,()))))
K11((Args (EqR,())),(Result (EqR,()))) is non empty Relation-like set
K10(K11((Args (EqR,())),(Result (EqR,())))) is non empty set
the_result_sort_of EqR is Element of the carrier of S

product (Carrier (A,())) is non empty functional with_common_domain product-like set
U1 is Relation-like Function-like Element of Args (EqR,())
(Den (EqR,())) . U1 is Element of Result (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

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,()), the ResultSort of S * ()
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,()) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,()) 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 * () is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (),(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,()) is non empty functional Element of rng K186( the carrier of S, the Sorts of ())
the Sorts of () 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 ()) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of ()) 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,())

(commute U19) . EqR is Relation-like Function-like 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

(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

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