:: 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₁)) where b₁ is Element of I : verum } is set
union { (rng (S . b₁)) where b₁ is Element of I : verum } is set
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₁)) where b₁ 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
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₁)) where b₁ 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,b₁) where b₁ is Element of the carrier' of I : ( the_result_sort_of b₁ = A & the_arity_of b₁ = {} ) } 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
{ b₁ where b₁ is Element of U1 : ex b₂ being Element of the carrier' of I st
( the Arity of I . b₂ = {} & the ResultSort of I . b₂ = A & b₁ in rng (Den (b₂,S)) ) } is set
U1 is non empty set
{ b₁ where b₁ is Element of U1 : ex b₂ being Element of the carrier' of I st
( the Arity of I . b₂ = {} & the ResultSort of I . b₂ = A & b₁ in rng (Den (b₂,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
{ b₁ where b₁ is Element of U2 : ex b₂ being Element of the carrier' of I st
( the Arity of I . b₂ = {} & the ResultSort of I . b₂ = A & b₁ in rng (Den (b₂,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
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₁))) where b₁ is Element of I : verum } is set
union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } is set
Funcs ({{}},(union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } )) is set
Funcs (I,(Funcs ({{}},(union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } )))) is set
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₁))) where b₁ is Element of I : verum } is set
union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } is set
Funcs (I,(union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } )) is 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
Funcs ({{}},(union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } )) is set
Funcs (I,(Funcs ({{}},(union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } )))) is set
(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₁))) where b₁ is Element of I : verum } )))) is set
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₁))) where b₁ is Element of S : verum } is set
union { (Result (A,(EqR . b₁))) where b₁ is Element of S : verum } is set
Funcs (S,(union { (Result (A,(EqR . b₁))) where b₁ is Element of S : verum } )) is set
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₁))) where b₁ is Element of I : verum } is set
union { (Result (U1,(EqR . b₁))) where b₁ is Element of I : verum } is set
Funcs ({{}},(union { (Result (U1,(EqR . b₁))) where b₁ is Element of I : verum } )) is set
Funcs (I,(Funcs ({{}},(union { (Result (U1,(EqR . b₁))) where b₁ is Element of I : verum } )))) is set
(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₁))) where b₁ is Element of I : verum } is set
union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } is set
Funcs (I,(union { (Result (EqR,(A . b₁))) where b₁ is Element of I : verum } )) is set
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₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
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₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
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₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ 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 . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ 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
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₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
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₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
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 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
U1 is Element of 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
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))
dom (the_arity_of U1) is countable Element of K10(K160())
U2 is Relation-like Function-like Element of Args (U1,(product A))
commute U2 is Relation-like Function-like Function-yielding V54() set
(commute U2) . EqR is Relation-like Function-like set
U19 is set
U2 . U19 is set
((commute U2) . EqR) . U19 is set
{ ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs ((dom (the_arity_of U1)),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
F is Relation-like Function-like set
F . 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 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))
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
U1 is Relation-like Function-like Element of Args (EqR,(product A))
(Den (EqR,(product A))) . U1 is Element of Result (EqR,(product A))
commute U1 is Relation-like Function-like Function-yielding V54() set
U2 is Element of I
A . U2 is non-empty MSAlgebra over S
Den (EqR,(A . U2)) is Relation-like Args (EqR,(A . U2)) -defined Result (EqR,(A . U2)) -valued Function-like quasi_total Element of K10(K11((Args (EqR,(A . U2))),(Result (EqR,(A . U2)))))
Args (EqR,(A . U2)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . U2))
the Sorts of (A . U2) 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 . U2)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (A . U2)) is set
Result (EqR,(A . U2)) is non empty Element of rng the Sorts of (A . U2)
rng the Sorts of (A . U2) is non empty with_non-empty_elements non empty-membered set
K11((Args (EqR,(A . U2))),(Result (EqR,(A . U2)))) is non empty Relation-like set
K10(K11((Args (EqR,(A . U2))),(Result (EqR,(A . U2))))) is non empty set
(commute U1) . U2 is Relation-like Function-like set
(Den (EqR,(A . U2))) . ((commute U1) . U2) is set
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
(OPS A) . EqR is set
commute (A ?. EqR) is Relation-like Function-like Function-yielding V54() set
IFEQ ((the_arity_of EqR),{},(commute (A ?. EqR)),(Commute (Frege (A ?. EqR)))) is set
dom (A ?. EqR) is non empty Element of K10(I)
K10(I) is non empty set
U19 is Relation-like Function-like set
U19 . U2 is set
(Frege (A ?. EqR)) . (commute U1) is Relation-like Function-like set
(A ?. EqR) .. (commute U1) is Relation-like Function-like set
(A ?. EqR) . U2 is Relation-like Function-like set
((A ?. EqR) . U2) . ((commute U1) . U2) 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
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
the Sorts of (product A) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
EqR is Element of I
A . EqR is non-empty MSAlgebra over S
the Sorts of (A . EqR) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is set
U1 . U2 is set
the Sorts of (product A) . U2 is set
the Sorts of (A . EqR) . U2 is set
K11(( the Sorts of (product A) . U2),( the Sorts of (A . EqR) . U2)) is Relation-like set
K10(K11(( the Sorts of (product A) . U2),( the Sorts of (A . EqR) . U2))) is non empty set
U19 is Element of the carrier of S
Carrier (A,U19) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
proj ((Carrier (A,U19)),EqR) is non empty Relation-like product (Carrier (A,U19)) -defined Function-like total set
product (Carrier (A,U19)) is non empty functional with_common_domain product-like set
U29 is Relation-like Function-like set
rng U29 is set
F is set
dom (Carrier (A,U19)) is non empty Element of K10(I)
K10(I) is non empty set
(Carrier (A,U19)) . EqR is non empty set
rng (proj ((Carrier (A,U19)),EqR)) is non empty set
dom (proj ((Carrier (A,U19)),EqR)) is non empty functional with_common_domain Element of K10((product (Carrier (A,U19))))
K10((product (Carrier (A,U19)))) is non empty set
s is set
(proj ((Carrier (A,U19)),EqR)) . s is set
s9 is Relation-like Function-like set
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 . U19 is set
dom U29 is set
dom (proj ((Carrier (A,U19)),EqR)) is non empty functional with_common_domain Element of K10((product (Carrier (A,U19))))
K10((product (Carrier (A,U19)))) is non empty set
U2 is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product A), the Sorts of (A . EqR)
U19 is Element of the carrier of S
U2 . U19 is Relation-like the Sorts of (product A) . U19 -defined the Sorts of (A . EqR) . U19 -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . U19),( the Sorts of (A . EqR) . U19)))
the Sorts of (product A) . U19 is non empty set
the Sorts of (A . EqR) . U19 is non empty set
K11(( the Sorts of (product A) . U19),( the Sorts of (A . EqR) . U19)) is non empty Relation-like set
K10(K11(( the Sorts of (product A) . U19),( the Sorts of (A . EqR) . U19))) is non empty set
Carrier (A,U19) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
proj ((Carrier (A,U19)),EqR) is non empty Relation-like product (Carrier (A,U19)) -defined Function-like total set
product (Carrier (A,U19)) is non empty functional with_common_domain product-like set
U1 is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product A), the Sorts of (A . EqR)
U2 is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product A), the Sorts of (A . EqR)
U19 is set
U1 . U19 is Relation-like Function-like set
U29 is Element of the carrier of S
Carrier (A,U29) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
proj ((Carrier (A,U29)),EqR) is non empty Relation-like product (Carrier (A,U29)) -defined Function-like total set
product (Carrier (A,U29)) is non empty functional with_common_domain product-like set
U2 . U19 is Relation-like Function-like 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))
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₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
U19 is Element of I
A . U19 is non-empty MSAlgebra over S
(I,S,A,U19) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product A), 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
(I,S,A,U19) # U1 is Relation-like Function-like Element of Args (EqR,(A . U19))
Args (EqR,(A . U19)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . U19))
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
(commute U1) . U19 is Relation-like Function-like set
dom (the_arity_of EqR) is countable Element of K10(K160())
Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs ((dom (the_arity_of EqR)),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs ((dom (the_arity_of EqR)),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
dom (commute U1) is set
rng (commute U1) is set
rng U1 is set
U29 is set
U1 . U29 is set
(the_arity_of EqR) /. U29 is Element of the carrier of S
Carrier (A,((the_arity_of EqR) /. U29)) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,((the_arity_of EqR) /. U29))) is non empty functional with_common_domain product-like set
proj ((Carrier (A,((the_arity_of EqR) /. U29))),U19) is non empty Relation-like product (Carrier (A,((the_arity_of EqR) /. U29))) -defined Function-like total set
dom (proj ((Carrier (A,((the_arity_of EqR) /. U29))),U19)) is non empty functional with_common_domain Element of K10((product (Carrier (A,((the_arity_of EqR) /. U29)))))
K10((product (Carrier (A,((the_arity_of EqR) /. U29))))) is non empty set
dom U1 is set
F is Relation-like Function-like set
dom F is set
rng F is set
((I,S,A,U19) # U1) . U29 is set
(I,S,A,U19) . ((the_arity_of EqR) /. U29) is Relation-like the Sorts of (product A) . ((the_arity_of EqR) /. U29) -defined the Sorts of (A . U19) . ((the_arity_of EqR) /. U29) -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . ((the_arity_of EqR) /. U29)),( the Sorts of (A . U19) . ((the_arity_of EqR) /. U29))))
the Sorts of (product A) . ((the_arity_of EqR) /. U29) is non empty set
the Sorts of (A . U19) . ((the_arity_of EqR) /. U29) is non empty set
K11(( the Sorts of (product A) . ((the_arity_of EqR) /. U29)),( the Sorts of (A . U19) . ((the_arity_of EqR) /. U29))) is non empty Relation-like set
K10(K11(( the Sorts of (product A) . ((the_arity_of EqR) /. U29)),( the Sorts of (A . U19) . ((the_arity_of EqR) /. U29)))) is non empty set
((I,S,A,U19) . ((the_arity_of EqR) /. U29)) . (U1 . U29) is set
(proj ((Carrier (A,((the_arity_of EqR) /. U29))),U19)) . (U1 . U29) is set
F . U19 is set
((commute U1) . U19) . U29 is set
(the_arity_of EqR) * (I,S,A,U19) is Relation-like K160() -defined Function-like Function-yielding V54() set
doms ((the_arity_of EqR) * (I,S,A,U19)) is Relation-like Function-like set
product (doms ((the_arity_of EqR) * (I,S,A,U19))) is functional with_common_domain product-like set
dom ((commute U1) . U19) is set
dom (I,S,A,U19) 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 ((I,S,A,U19) # U1) is set
Frege ((the_arity_of EqR) * (I,S,A,U19)) is Relation-like product (doms ((the_arity_of EqR) * (I,S,A,U19))) -defined Function-like total Function-yielding V54() set
(Frege ((the_arity_of EqR) * (I,S,A,U19))) . U1 is Relation-like Function-like set
dom ((Frege ((the_arity_of EqR) * (I,S,A,U19))) . U1) is set
((the_arity_of EqR) * (I,S,A,U19)) .. U1 is Relation-like Function-like set
dom (((the_arity_of EqR) * (I,S,A,U19)) .. U1) is set
dom ((the_arity_of EqR) * (I,S,A,U19)) is countable Element of K10(K160())
I is non empty set
S is non empty non void V68() ManySortedSign
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 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 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
(I,S,EqR,A) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product EqR), the Sorts of (EqR . A)
the Sorts of (product EqR) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of (EqR . A) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 is Element of the carrier' of S
Args (U1,(product EqR)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product EqR))
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
the_result_sort_of U1 is Element of the carrier of S
(I,S,EqR,A) . (the_result_sort_of U1) is Relation-like the Sorts of (product EqR) . (the_result_sort_of U1) -defined the Sorts of (EqR . A) . (the_result_sort_of U1) -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product EqR) . (the_result_sort_of U1)),( the Sorts of (EqR . A) . (the_result_sort_of U1))))
the Sorts of (product EqR) . (the_result_sort_of U1) is non empty set
the Sorts of (EqR . A) . (the_result_sort_of U1) is non empty set
K11(( the Sorts of (product EqR) . (the_result_sort_of U1)),( the Sorts of (EqR . A) . (the_result_sort_of U1))) is non empty Relation-like set
K10(K11(( the Sorts of (product EqR) . (the_result_sort_of U1)),( the Sorts of (EqR . A) . (the_result_sort_of U1)))) is non empty 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)))))
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,(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))
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
U2 is Relation-like Function-like Element of Args (U1,(product EqR))
(Den (U1,(product EqR))) . U2 is set
((I,S,EqR,A) . (the_result_sort_of U1)) . ((Den (U1,(product EqR))) . U2) is set
(I,S,EqR,A) # U2 is Relation-like Function-like Element of Args (U1,(EqR . A))
(Den (U1,(EqR . A))) . ((I,S,EqR,A) # U2) is set
dom the ResultSort of S is Element of K10( the carrier' of S)
K10( the carrier' of S) is non empty set
the ResultSort of S * the Sorts of (product EqR) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the ResultSort of S * the Sorts of (product EqR)) . U1 is non empty set
the ResultSort of S . U1 is Element of the carrier of S
the Sorts of (product EqR) . ( the ResultSort of S . U1) is non empty set
(SORTS EqR) . (the_result_sort_of U1) is non empty set
Carrier (EqR,(the_result_sort_of U1)) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (EqR,(the_result_sort_of U1))) is non empty functional with_common_domain product-like set
(Den (U1,(product EqR))) . U2 is Element of Result (U1,(product EqR))
((I,S,EqR,A) . (the_result_sort_of U1)) . ((Den (U1,(product EqR))) . U2) is set
(Den (U1,(EqR . A))) . ((I,S,EqR,A) # U2) is Element of Result (U1,(EqR . A))
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 set
proj ((Carrier (EqR,(the_result_sort_of U1))),A) is non empty Relation-like product (Carrier (EqR,(the_result_sort_of U1))) -defined Function-like total set
dom (proj ((Carrier (EqR,(the_result_sort_of U1))),A)) is non empty functional with_common_domain Element of K10((product (Carrier (EqR,(the_result_sort_of U1)))))
K10((product (Carrier (EqR,(the_result_sort_of U1))))) is non empty set
((I,S,EqR,A) . (the_result_sort_of U1)) . (S,(product EqR),U1) is set
(proj ((Carrier (EqR,(the_result_sort_of U1))),A)) . (S,(product EqR),U1) is set
(S,(product EqR),U1) . A is set
(S,(EqR . A),U1) is set
(Den (U1,(EqR . A))) . {} is set
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))
proj ((Carrier (EqR,(the_result_sort_of U1))),A) is non empty Relation-like product (Carrier (EqR,(the_result_sort_of U1))) -defined Function-like total set
dom (proj ((Carrier (EqR,(the_result_sort_of U1))),A)) is non empty functional with_common_domain Element of K10((product (Carrier (EqR,(the_result_sort_of U1)))))
K10((product (Carrier (EqR,(the_result_sort_of U1))))) is non empty set
(proj ((Carrier (EqR,(the_result_sort_of U1))),A)) . ((Den (U1,(product EqR))) . U2) is set
F is Relation-like Function-like set
F . A is set
commute U2 is Relation-like Function-like Function-yielding V54() set
(commute U2) . A is Relation-like Function-like set
(Den (U1,(EqR . A))) . ((commute U2) . A) is set
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))
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
U1 is Element of the carrier of S
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U19 is non empty Relation-like I -defined Function-like total Function-yielding V54() set
{ ((U19 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } is set
Funcs ( the carrier of S, { ((U19 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } ) is set
Funcs (I,(Funcs ( the carrier of S, { ((U19 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } ))) is set
commute U19 is Relation-like Function-like Function-yielding V54() set
(commute U19) . U1 is Relation-like Function-like set
((commute U19) . U1) . A is set
U19 . A is Relation-like Function-like set
(U19 . A) . U1 is set
rng U19 is non empty set
s is set
dom U19 is non empty Element of K10(I)
K10(I) is non empty set
s9 is set
U19 . s9 is Relation-like Function-like set
f is Element of I
EqR . f is non-empty MSAlgebra over S
the Sorts of (EqR . f) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U19 . f is Relation-like Function-like set
y is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of U2, the Sorts of (EqR . f)
rng y is non empty set
x is set
dom y is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
x is set
y . x is Relation-like Function-like set
dom y is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
dom U19 is non empty Element of K10(I)
K10(I) 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
{ ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
EqR is Element of the carrier of S
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of U1 . EqR is non empty set
Funcs (( the Sorts of U1 . EqR),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs (( the Sorts of U1 . EqR),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
U2 is non empty Relation-like I -defined Function-like total Function-yielding V54() set
commute U2 is Relation-like Function-like Function-yielding V54() set
(commute U2) . EqR is Relation-like Function-like set
{ ((U2 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } is set
Funcs ( the carrier of S, { ((U2 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } ) is set
Funcs (I,(Funcs ( the carrier of S, { ((U2 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } ))) is set
Funcs (I, { ((U2 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } ) is set
Funcs ( the carrier of S,(Funcs (I, { ((U2 . b₂) . b₁) where b₁ is Element of the carrier of S, b₂ is Element of I : verum } ))) is set
f is Relation-like Function-like set
dom f is set
rng f is set
rng ((commute U2) . EqR) is set
y is set
dom ((commute U2) . EqR) is set
x is set
((commute U2) . EqR) . x is set
f9 is Relation-like Function-like set
dom f9 is set
rng f9 is set
x is Element of I
A . x is non-empty MSAlgebra over S
the Sorts of (A . x) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 . x is Relation-like Function-like set
f9 is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of U1, the Sorts of (A . x)
the Sorts of (A . x) . EqR is non empty set
e is set
f9 . EqR is Relation-like the Sorts of U1 . EqR -defined the Sorts of (A . x) . EqR -valued Function-like quasi_total Element of K10(K11(( the Sorts of U1 . EqR),( the Sorts of (A . x) . EqR)))
K11(( the Sorts of U1 . EqR),( the Sorts of (A . x) . EqR)) is non empty Relation-like set
K10(K11(( the Sorts of U1 . EqR),( the Sorts of (A . x) . EqR))) is non empty set
dom (f9 . EqR) is Element of K10(( the Sorts of U1 . EqR))
K10(( the Sorts of U1 . EqR)) is non empty set
rng (f9 . EqR) is Element of K10(( the Sorts of (A . x) . EqR))
K10(( the Sorts of (A . x) . EqR)) is non empty set
y is Relation-like Function-like set
dom y is set
rng y 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 Element of I
EqR is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S
EqR . A is non-empty MSAlgebra over S
the Sorts of (EqR . A) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 is Element of the carrier of S
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of U2 . U1 is non empty set
{ ( the Sorts of (EqR . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (EqR . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
F is non empty Relation-like I -defined Function-like total Function-yielding V54() set
F . A is Relation-like Function-like set
commute F is Relation-like Function-like Function-yielding V54() set
(commute F) . U1 is Relation-like Function-like set
commute ((commute F) . U1) is Relation-like Function-like Function-yielding V54() set
Funcs (( the Sorts of U2 . U1),(union { ( the Sorts of (EqR . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs (( the Sorts of U2 . U1),(union { ( the Sorts of (EqR . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
dom ((commute F) . U1) is set
((commute F) . U1) . A is set
rng ((commute F) . U1) is set
s is Relation-like Function-like set
s . A is set
s9 is Relation-like Function-like set
dom s9 is set
rng s9 is set
f is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of U2, the Sorts of (EqR . A)
f . U1 is Relation-like the Sorts of U2 . U1 -defined the Sorts of (EqR . A) . U1 -valued Function-like quasi_total Element of K10(K11(( the Sorts of U2 . U1),( the Sorts of (EqR . A) . U1)))
the Sorts of (EqR . A) . U1 is non empty set
K11(( the Sorts of U2 . U1),( the Sorts of (EqR . A) . U1)) is non empty Relation-like set
K10(K11(( the Sorts of U2 . U1),( the Sorts of (EqR . A) . U1))) is non empty set
y is set
(commute ((commute F) . U1)) . y is Relation-like Function-like set
(f . U1) . y is set
x is Relation-like Function-like set
x . 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
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
product (Carrier (A,EqR)) is non empty functional with_common_domain product-like set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of U1 . EqR is non empty set
{ ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
U29 is non empty Relation-like I -defined Function-like total Function-yielding V54() set
commute U29 is Relation-like Function-like Function-yielding V54() set
(commute U29) . EqR is Relation-like Function-like set
commute ((commute U29) . EqR) is Relation-like Function-like Function-yielding V54() set
Funcs (( the Sorts of U1 . EqR),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs (( the Sorts of U1 . EqR),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (( the Sorts of U1 . EqR),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
F is Relation-like Function-like set
dom F is set
rng F is set
s is set
(commute ((commute U29) . EqR)) . s is Relation-like Function-like set
F . s is set
s9 is Relation-like Function-like set
dom s9 is set
rng s9 is set
f is set
dom (Carrier (A,EqR)) is non empty Element of K10(I)
K10(I) is non empty set
y is Element of I
A . y is non-empty MSAlgebra over S
the Sorts of (A . y) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U29 . y is Relation-like Function-like set
x is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of U1, the Sorts of (A . y)
x . EqR is Relation-like the Sorts of U1 . EqR -defined the Sorts of (A . y) . EqR -valued Function-like quasi_total Element of K10(K11(( the Sorts of U1 . EqR),( the Sorts of (A . y) . EqR)))
the Sorts of (A . y) . EqR is non empty set
K11(( the Sorts of U1 . EqR),( the Sorts of (A . y) . EqR)) is non empty Relation-like set
K10(K11(( the Sorts of U1 . EqR),( the Sorts of (A . y) . EqR))) is non empty set
dom (x . EqR) is Element of K10(( the Sorts of U1 . EqR))
K10(( the Sorts of U1 . EqR)) is non empty set
(Carrier (A,EqR)) . y is non empty set
(x . EqR) . s is set
rng (x . EqR) is Element of K10(( the Sorts of (A . y) . EqR))
K10(( the Sorts of (A . y) . EqR)) is non empty set
s9 . y is set
((commute ((commute U29) . EqR)) . s) . f is set
(Carrier (A,EqR)) . f is 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 . EqR is set
dom ((commute ((commute U29) . EqR)) . s) 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
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
the Sorts of (product A) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
EqR is non-empty MSAlgebra over S
the Sorts of EqR is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 is non empty Relation-like I -defined Function-like total Function-yielding V54() set
{ ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } is set
commute U1 is Relation-like Function-like Function-yielding V54() set
F is non empty Relation-like the carrier of S -defined Function-like total set
s is set
(commute U1) . s is Relation-like Function-like set
the Sorts of EqR . s is set
Funcs (( the Sorts of EqR . s),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs (( the Sorts of EqR . s),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
commute ((commute U1) . s) is Relation-like Function-like Function-yielding V54() set
Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (( the Sorts of EqR . s),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
F . s is set
f is Relation-like Function-like set
dom f is set
rng f is set
the Sorts of (product A) . s is set
y is set
x is Relation-like Function-like set
dom x is set
rng x is set
x is set
f . x is set
f9 is set
s9 is Element of the carrier of S
Carrier (A,s9) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
dom (Carrier (A,s9)) is non empty Element of K10(I)
K10(I) is non empty set
e is Element of I
A . e is non-empty MSAlgebra over S
the Sorts of (A . e) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 . e is Relation-like Function-like set
e is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of EqR, the Sorts of (A . e)
F . s9 is set
(commute U1) . s9 is Relation-like Function-like set
commute ((commute U1) . s9) is Relation-like Function-like Function-yielding V54() set
x . e is set
e . s9 is Relation-like the Sorts of EqR . s9 -defined the Sorts of (A . e) . s9 -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . s9),( the Sorts of (A . e) . s9)))
the Sorts of EqR . s9 is non empty set
the Sorts of (A . e) . s9 is non empty set
K11(( the Sorts of EqR . s9),( the Sorts of (A . e) . s9)) is non empty Relation-like set
K10(K11(( the Sorts of EqR . s9),( the Sorts of (A . e) . s9))) is non empty set
(e . s9) . x is set
dom (e . s9) is Element of K10(( the Sorts of EqR . s9))
K10(( the Sorts of EqR . s9)) is non empty set
e . s is Relation-like Function-like set
(e . s) . x is set
rng (e . s) is set
(Carrier (A,s9)) . e is non empty set
rng (e . s9) is Element of K10(( the Sorts of (A . e) . s9))
K10(( the Sorts of (A . e) . s9)) is non empty set
x . f9 is set
(Carrier (A,s9)) . f9 is set
Ji is MSAlgebra over S
the Sorts of Ji is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of Ji . s9 is set
product (Carrier (A,s9)) is non empty functional with_common_domain product-like set
K11(( the Sorts of EqR . s),( the Sorts of (product A) . s)) is Relation-like set
K10(K11(( the Sorts of EqR . s),( the Sorts of (product A) . s))) is non empty set
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of EqR, the Sorts of (product A)
s9 is Element of the carrier' of S
Args (s9,EqR) is non empty functional Element of rng K186( the carrier of S, the Sorts of EqR)
K186( the carrier of S, the Sorts of EqR) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of EqR) is set
the_result_sort_of s9 is Element of the carrier of S
s . (the_result_sort_of s9) is Relation-like the Sorts of EqR . (the_result_sort_of s9) -defined the Sorts of (product A) . (the_result_sort_of s9) -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (product A) . (the_result_sort_of s9))))
the Sorts of EqR . (the_result_sort_of s9) is non empty set
the Sorts of (product A) . (the_result_sort_of s9) is non empty set
K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (product A) . (the_result_sort_of s9))) is non empty Relation-like set
K10(K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (product A) . (the_result_sort_of s9)))) is non empty set
Den (s9,EqR) is Relation-like Args (s9,EqR) -defined Result (s9,EqR) -valued Function-like quasi_total Element of K10(K11((Args (s9,EqR)),(Result (s9,EqR))))
Result (s9,EqR) is non empty Element of rng the Sorts of EqR
rng the Sorts of EqR is non empty with_non-empty_elements non empty-membered set
K11((Args (s9,EqR)),(Result (s9,EqR))) is non empty Relation-like set
K10(K11((Args (s9,EqR)),(Result (s9,EqR)))) is non empty set
Den (s9,(product A)) is Relation-like Args (s9,(product A)) -defined Result (s9,(product A)) -valued Function-like quasi_total Element of K10(K11((Args (s9,(product A))),(Result (s9,(product A)))))
Args (s9,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))
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 (s9,(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 (s9,(product A))),(Result (s9,(product A)))) is non empty Relation-like set
K10(K11((Args (s9,(product A))),(Result (s9,(product A))))) is non empty set
f is Relation-like Function-like Element of Args (s9,EqR)
(Den (s9,EqR)) . f is set
(s . (the_result_sort_of s9)) . ((Den (s9,EqR)) . f) is set
s # f is Relation-like Function-like Element of Args (s9,(product A))
(Den (s9,(product A))) . (s # f) is set
(Den (s9,EqR)) . f is Element of Result (s9,EqR)
(s . (the_result_sort_of s9)) . ((Den (s9,EqR)) . f) is set
(Den (s9,(product A))) . (s # f) is Element of Result (s9,(product A))
the_arity_of s9 is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))
(commute U1) . (the_result_sort_of s9) is Relation-like Function-like set
commute ((commute U1) . (the_result_sort_of s9)) is Relation-like Function-like Function-yielding V54() set
(S,EqR,s9) is set
(Den (s9,EqR)) . {} is set
(commute ((commute U1) . (the_result_sort_of s9))) . (S,EqR,s9) is Relation-like Function-like set
x is set
f9 is Element of I
A . f9 is non-empty MSAlgebra over S
the Sorts of (A . f9) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 . f9 is Relation-like Function-like set
e is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of EqR, the Sorts of (A . f9)
e # f is Relation-like Function-like Element of Args (s9,(A . f9))
Args (s9,(A . f9)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . f9))
K186( the carrier of S, the Sorts of (A . f9)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (A . f9)) is set
((commute ((commute U1) . (the_result_sort_of s9))) . (S,EqR,s9)) . x is set
e . (the_result_sort_of s9) is Relation-like the Sorts of EqR . (the_result_sort_of s9) -defined the Sorts of (A . f9) . (the_result_sort_of s9) -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (A . f9) . (the_result_sort_of s9))))
the Sorts of (A . f9) . (the_result_sort_of s9) is non empty set
K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (A . f9) . (the_result_sort_of s9))) is non empty Relation-like set
K10(K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (A . f9) . (the_result_sort_of s9)))) is non empty set
(e . (the_result_sort_of s9)) . ((Den (s9,EqR)) . f) is set
(S,(A . f9),s9) is set
Den (s9,(A . f9)) is Relation-like Args (s9,(A . f9)) -defined Result (s9,(A . f9)) -valued Function-like quasi_total Element of K10(K11((Args (s9,(A . f9))),(Result (s9,(A . f9)))))
Result (s9,(A . f9)) is non empty Element of rng the Sorts of (A . f9)
rng the Sorts of (A . f9) is non empty with_non-empty_elements non empty-membered set
K11((Args (s9,(A . f9))),(Result (s9,(A . f9)))) is non empty Relation-like set
K10(K11((Args (s9,(A . f9))),(Result (s9,(A . f9))))) is non empty set
(Den (s9,(A . f9))) . {} is set
(S,(product A),s9) is Relation-like Function-like set
(Den (s9,(product A))) . {} is set
(S,(product A),s9) . x is set
{ (Result (s9,(A . b₁))) where b₁ is Element of I : verum } is set
union { (Result (s9,(A . b₁))) where b₁ is Element of I : verum } is set
Funcs (I,(union { (Result (s9,(A . b₁))) where b₁ is Element of I : verum } )) is set
Carrier (A,(the_result_sort_of s9)) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,(the_result_sort_of s9))) is non empty functional with_common_domain product-like set
dom ((commute ((commute U1) . (the_result_sort_of s9))) . (S,EqR,s9)) is set
dom (Carrier (A,(the_result_sort_of s9))) is non empty Element of K10(I)
K10(I) is non empty set
x is Relation-like Function-like set
dom x is set
rng x is set
the_arity_of s9 is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))
(OPS A) . s9 is set
A ?. s9 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)) . s9 is Relation-like Function-like set
commute (A ?. s9) is Relation-like Function-like Function-yielding V54() set
Frege (A ?. s9) is Relation-like product (doms (A ?. s9)) -defined Function-like total Function-yielding V54() set
doms (A ?. s9) is Relation-like Function-like set
product (doms (A ?. s9)) is functional with_common_domain product-like set
Commute (Frege (A ?. s9)) is Relation-like Function-like set
IFEQ ((the_arity_of s9),{},(commute (A ?. s9)),(Commute (Frege (A ?. s9)))) is set
x is Relation-like Function-like Element of Args (s9,(product A))
commute x is Relation-like Function-like Function-yielding V54() set
dom (Frege (A ?. s9)) is functional with_common_domain Element of K10((product (doms (A ?. s9))))
K10((product (doms (A ?. s9)))) is non empty set
dom (Commute (Frege (A ?. s9))) is set
(Den (s9,(product A))) . x is Element of Result (s9,(product A))
(Frege (A ?. s9)) . (commute x) is Relation-like Function-like set
rng (Frege (A ?. s9)) is set
x is Relation-like Function-like set
dom x is set
(commute U1) . (the_result_sort_of s9) is Relation-like Function-like set
commute ((commute U1) . (the_result_sort_of s9)) is Relation-like Function-like Function-yielding V54() set
(commute ((commute U1) . (the_result_sort_of s9))) . ((Den (s9,EqR)) . f) is Relation-like Function-like set
dom (the_arity_of s9) is countable Element of K10(K160())
Funcs ((dom (the_arity_of s9)),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
e is set
e is Element of I
A . e is non-empty MSAlgebra over S
the Sorts of (A . e) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 . e is Relation-like Function-like set
Ji is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of EqR, the Sorts of (A . e)
Ji . (the_result_sort_of s9) is Relation-like the Sorts of EqR . (the_result_sort_of s9) -defined the Sorts of (A . e) . (the_result_sort_of s9) -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (A . e) . (the_result_sort_of s9))))
the Sorts of (A . e) . (the_result_sort_of s9) is non empty set
K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (A . e) . (the_result_sort_of s9))) is non empty Relation-like set
K10(K11(( the Sorts of EqR . (the_result_sort_of s9)),( the Sorts of (A . e) . (the_result_sort_of s9)))) is non empty set
(Ji . (the_result_sort_of s9)) . ((Den (s9,EqR)) . f) is set
Args (s9,(A . e)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . e))
K186( the carrier of S, the Sorts of (A . e)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (A . e)) is set
Result (s9,(A . e)) is non empty Element of rng the Sorts of (A . e)
rng the Sorts of (A . e) is non empty with_non-empty_elements non empty-membered set
Den (s9,(A . e)) is Relation-like Args (s9,(A . e)) -defined Result (s9,(A . e)) -valued Function-like quasi_total Element of K10(K11((Args (s9,(A . e))),(Result (s9,(A . e)))))
K11((Args (s9,(A . e))),(Result (s9,(A . e)))) is non empty Relation-like set
K10(K11((Args (s9,(A . e))),(Result (s9,(A . e))))) is non empty set
Ji # f is Relation-like Function-like Element of Args (s9,(A . e))
(Den (s9,(A . e))) . (Ji # f) is Element of Result (s9,(A . e))
Cs is set
(the_arity_of s9) . Cs is set
rng (the_arity_of s9) is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
(Ji # f) . Cs is set
(the_arity_of s9) /. Cs is Element of the carrier of S
Ji . ((the_arity_of s9) /. Cs) is Relation-like the Sorts of EqR . ((the_arity_of s9) /. Cs) -defined the Sorts of (A . e) . ((the_arity_of s9) /. Cs) -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . ((the_arity_of s9) /. Cs)),( the Sorts of (A . e) . ((the_arity_of s9) /. Cs))))
the Sorts of EqR . ((the_arity_of s9) /. Cs) is non empty set
the Sorts of (A . e) . ((the_arity_of s9) /. Cs) is non empty set
K11(( the Sorts of EqR . ((the_arity_of s9) /. Cs)),( the Sorts of (A . e) . ((the_arity_of s9) /. Cs))) is non empty Relation-like set
K10(K11(( the Sorts of EqR . ((the_arity_of s9) /. Cs)),( the Sorts of (A . e) . ((the_arity_of s9) /. Cs)))) is non empty set
f . Cs is set
(Ji . ((the_arity_of s9) /. Cs)) . (f . Cs) is set
y9 is Element of the carrier of S
Ji . y9 is Relation-like the Sorts of EqR . y9 -defined the Sorts of (A . e) . y9 -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . y9),( the Sorts of (A . e) . y9)))
the Sorts of EqR . y9 is non empty set
the Sorts of (A . e) . y9 is non empty set
K11(( the Sorts of EqR . y9),( the Sorts of (A . e) . y9)) is non empty Relation-like set
K10(K11(( the Sorts of EqR . y9),( the Sorts of (A . e) . y9))) is non empty set
(Ji . y9) . (f . Cs) is set
(the_arity_of s9) * the Sorts of EqR is Relation-like non-empty K160() -defined Function-like set
product ((the_arity_of s9) * the Sorts of EqR) is non empty functional with_common_domain product-like set
dom f is set
dom ((the_arity_of s9) * the Sorts of EqR) is countable Element of K10(K160())
((the_arity_of s9) * the Sorts of EqR) . Cs is set
(s # f) . Cs is set
s . ((the_arity_of s9) /. Cs) is Relation-like the Sorts of EqR . ((the_arity_of s9) /. Cs) -defined the Sorts of (product A) . ((the_arity_of s9) /. Cs) -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . ((the_arity_of s9) /. Cs)),( the Sorts of (product A) . ((the_arity_of s9) /. Cs))))
the Sorts of (product A) . ((the_arity_of s9) /. Cs) is non empty set
K11(( the Sorts of EqR . ((the_arity_of s9) /. Cs)),( the Sorts of (product A) . ((the_arity_of s9) /. Cs))) is non empty Relation-like set
K10(K11(( the Sorts of EqR . ((the_arity_of s9) /. Cs)),( the Sorts of (product A) . ((the_arity_of s9) /. Cs)))) is non empty set
(s . ((the_arity_of s9) /. Cs)) . (f . Cs) is set
s . y9 is Relation-like the Sorts of EqR . y9 -defined the Sorts of (product A) . y9 -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . y9),( the Sorts of (product A) . y9)))
the Sorts of (product A) . y9 is non empty set
K11(( the Sorts of EqR . y9),( the Sorts of (product A) . y9)) is non empty Relation-like set
K10(K11(( the Sorts of EqR . y9),( the Sorts of (product A) . y9))) is non empty set
(s . y9) . (f . Cs) is set
(commute U1) . y9 is Relation-like Function-like set
commute ((commute U1) . y9) is Relation-like Function-like Function-yielding V54() set
(commute ((commute U1) . y9)) . (f . Cs) is Relation-like Function-like set
commute (s # f) is Relation-like Function-like Function-yielding V54() set
(commute (s # f)) . e is Relation-like Function-like set
((commute (s # f)) . e) . Cs is set
i is Relation-like Function-like set
i . e is set
dom Ji is non empty Element of K10( the carrier of S)
Funcs ((dom (the_arity_of s9)),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs ((dom (the_arity_of s9)),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
Cs is Relation-like Function-like set
dom Cs is set
rng Cs is set
Cs . e is set
(the_arity_of s9) * Ji is Relation-like K160() -defined Function-like Function-yielding V54() set
doms ((the_arity_of s9) * Ji) is Relation-like Function-like set
product (doms ((the_arity_of s9) * Ji)) is functional with_common_domain product-like set
dom (Ji # f) is set
Frege ((the_arity_of s9) * Ji) is Relation-like product (doms ((the_arity_of s9) * Ji)) -defined Function-like total Function-yielding V54() set
(Frege ((the_arity_of s9) * Ji)) . f is Relation-like Function-like set
dom ((Frege ((the_arity_of s9) * Ji)) . f) is set
((the_arity_of s9) * Ji) .. f is Relation-like Function-like set
dom (((the_arity_of s9) * Ji) .. f) is set
dom ((the_arity_of s9) * Ji) is countable Element of K10(K160())
y9 is Relation-like Function-like set
dom y9 is set
rng y9 is set
((commute ((commute U1) . (the_result_sort_of s9))) . ((Den (s9,EqR)) . f)) . e is set
(Den (s9,(A . e))) . ((commute (s # f)) . e) is set
x . e is set
Carrier (A,(the_result_sort_of s9)) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,(the_result_sort_of s9))) is non empty functional with_common_domain product-like set
dom ((commute ((commute U1) . (the_result_sort_of s9))) . ((Den (s9,EqR)) . f)) is set
dom (Carrier (A,(the_result_sort_of s9))) is non empty Element of K10(I)
K10(I) is non empty set
the_arity_of s9 is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))
s9 is Element of I
A . s9 is non-empty MSAlgebra over S
the Sorts of (A . s9) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(I,S,A,s9) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product A), the Sorts of (A . s9)
(I,S,A,s9) ** s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of EqR, the Sorts of (A . s9)
U1 . s9 is Relation-like Function-like set
f is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of EqR, the Sorts of (A . s9)
dom ((I,S,A,s9) ** s) is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
dom (I,S,A,s9) is non empty Element of K10( the carrier of S)
dom s is non empty Element of K10( the carrier of S)
(dom (I,S,A,s9)) /\ (dom s) is Element of K10( the carrier of S)
the carrier of S /\ (dom s) is Element of K10( the carrier of S)
the carrier of S /\ the carrier of S is set
y is set
((I,S,A,s9) ** s) . y is Relation-like Function-like set
x is Element of the carrier of S
the Sorts of EqR . x is non empty set
the Sorts of (product A) . x is non empty set
the Sorts of (A . s9) . x is non empty set
s . x is Relation-like the Sorts of EqR . x -defined the Sorts of (product A) . x -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . x),( the Sorts of (product A) . x)))
K11(( the Sorts of EqR . x),( the Sorts of (product A) . x)) is non empty Relation-like set
K10(K11(( the Sorts of EqR . x),( the Sorts of (product A) . x))) is non empty set
(I,S,A,s9) . x is Relation-like the Sorts of (product A) . x -defined the Sorts of (A . s9) . x -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . x),( the Sorts of (A . s9) . x)))
K11(( the Sorts of (product A) . x),( the Sorts of (A . s9) . x)) is non empty Relation-like set
K10(K11(( the Sorts of (product A) . x),( the Sorts of (A . s9) . x))) is non empty set
((I,S,A,s9) . x) * (s . x) is Relation-like the Sorts of EqR . x -defined the Sorts of (A . s9) . x -valued Function-like Element of K10(K11(( the Sorts of EqR . x),( the Sorts of (A . s9) . x)))
K11(( the Sorts of EqR . x),( the Sorts of (A . s9) . x)) is non empty Relation-like set
K10(K11(( the Sorts of EqR . x),( the Sorts of (A . s9) . x))) is non empty set
Carrier (A,x) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
proj ((Carrier (A,x)),s9) is non empty Relation-like product (Carrier (A,x)) -defined Function-like total set
product (Carrier (A,x)) is non empty functional with_common_domain product-like set
(s . x) * (proj ((Carrier (A,x)),s9)) is Relation-like the Sorts of EqR . x -defined Function-like set
(commute U1) . x is Relation-like Function-like set
commute ((commute U1) . x) is Relation-like Function-like Function-yielding V54() set
(commute ((commute U1) . x)) * (proj ((Carrier (A,x)),s9)) is Relation-like Function-like set
Funcs (( the Sorts of EqR . x),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )) is set
Funcs (I,(Funcs (( the Sorts of EqR . x),(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
Funcs (( the Sorts of EqR . x),(Funcs (I,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of I, b₂ is Element of the carrier of S : verum } )))) is set
x is Relation-like Function-like set
dom x is set
rng x is set
dom (proj ((Carrier (A,x)),s9)) is non empty functional with_common_domain Element of K10((product (Carrier (A,x))))
K10((product (Carrier (A,x)))) is non empty set
f9 is set
e is set
x . e is set
(commute ((commute U1) . x)) . e is Relation-like Function-like set
dom (((I,S,A,s9) ** s) . y) is set
the Sorts of EqR . y is set
f9 is set
(commute ((commute U1) . x)) . f9 is Relation-like Function-like set
(((I,S,A,s9) ** s) . y) . f9 is set
(proj ((Carrier (A,x)),s9)) . ((commute ((commute U1) . x)) . f9) is set
((commute ((commute U1) . x)) . f9) . s9 is set
f . y is Relation-like Function-like set
(f . y) . f9 is set
dom (f . y) is set
f . x is Relation-like the Sorts of EqR . x -defined the Sorts of (A . s9) . x -valued Function-like quasi_total Element of K10(K11(( the Sorts of EqR . x),( the Sorts of (A . s9) . x)))
dom (f . x) is Element of K10(( the Sorts of EqR . x))
K10(( the Sorts of EqR . x)) is non empty set
dom f is non empty Element of K10( the carrier of S)
s9 is Element of I
A . s9 is non-empty MSAlgebra over S
the Sorts of (A . s9) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(I,S,A,s9) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product A), the Sorts of (A . s9)
(I,S,A,s9) ** s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of EqR, the Sorts of (A . s9)
U1 . s9 is Relation-like Function-like set
I is non empty set
S is non empty Relation-like I -defined Function-like total set
A is non empty non void V68() ManySortedSign
EqR is set
S . EqR is set
the Relation-like S . EqR -defined Function-like total MSAlgebra-Family of S . EqR,A is Relation-like S . EqR -defined Function-like total MSAlgebra-Family of S . EqR,A
EqR is non empty Relation-like I -defined Function-like total set
U1 is set
EqR . U1 is set
S . U1 is set
I is non empty set
S is non empty non void V68() ManySortedSign
K11(I,I) is non empty Relation-like set
K10(K11(I,I)) is non empty set
EqR is Relation-like I -defined I -valued V12() V14() V19() total Element of K10(K11(I,I))
Class EqR is non empty with_non-empty_elements non empty-membered a_partition of I
id (Class EqR) is non empty Relation-like non-empty non empty-yielding Class EqR -defined Class EqR -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11((Class EqR),(Class EqR)))
K11((Class EqR),(Class EqR)) is non empty Relation-like set
K10(K11((Class EqR),(Class EqR))) is non empty set
A is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S
U1 is non empty Relation-like Class EqR -defined Function-like total set
U2 is set
U1 . U2 is set
(id (Class EqR)) . U2 is set
A | U2 is Relation-like U2 -defined I -defined Function-like set
dom (A | U2) is Element of K10(U2)
K10(U2) is non empty set
dom A is non empty Element of K10(I)
K10(I) is non empty set
(dom A) /\ U2 is Element of K10(I)
I /\ U2 is set
U19 is Relation-like (id (Class EqR)) . U2 -defined Function-like total set
U29 is set
U19 . U29 is set
dom U19 is Element of K10(((id (Class EqR)) . U2))
K10(((id (Class EqR)) . U2)) is non empty set
F is Element of I
A . F is non-empty MSAlgebra over S
U2 is non empty Relation-like Class EqR -defined Function-like total ( Class EqR, id (Class EqR),S)
U19 is set
U2 . U19 is set
A | U19 is Relation-like U19 -defined I -defined Function-like set
U1 is non empty Relation-like Class EqR -defined Function-like total ( Class EqR, id (Class EqR),S)
U2 is non empty Relation-like Class EqR -defined Function-like total ( Class EqR, id (Class EqR),S)
U19 is set
U1 . U19 is set
A | U19 is Relation-like U19 -defined I -defined Function-like set
U2 . U19 is set
U1 is non empty Relation-like Class EqR -defined Function-like total ( Class EqR, id (Class EqR),S)
U2 is non empty Relation-like Class EqR -defined Function-like total ( Class EqR, id (Class EqR),S)
I is non empty set
A is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
S is non empty non void V68() ManySortedSign
EqR is non empty Relation-like I -defined Function-like total (I,A,S)
U1 is set
A . U1 is set
U2 is non empty set
EqR . U1 is set
U19 is non empty Relation-like U2 -defined Function-like total MSAlgebra-Family of U2,S
product U19 is strict non-empty MSAlgebra over S
SORTS U19 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 U19 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 U19)), the ResultSort of S * (SORTS U19)
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 U19)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS U19)) 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 U19) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS U19),(OPS U19) #) is strict MSAlgebra over S
U29 is set
U29 is set
F is set
s is non empty set
s9 is non empty Relation-like s -defined Function-like total MSAlgebra-Family of s,S
product s9 is strict non-empty MSAlgebra over S
SORTS s9 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS s9 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 s9)), the ResultSort of S * (SORTS s9)
K186( the carrier of S,(SORTS s9)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS s9)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS s9) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS s9),(OPS s9) #) is strict MSAlgebra over S
U1 is non empty Relation-like I -defined Function-like total set
U2 is set
A . U2 is set
EqR . U2 is set
U1 . U2 is set
U19 is non empty set
U29 is non empty Relation-like U19 -defined Function-like total MSAlgebra-Family of U19,S
product U29 is strict non-empty MSAlgebra over S
SORTS U29 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS U29 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 U29)), the ResultSort of S * (SORTS U29)
K186( the carrier of S,(SORTS U29)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS U29)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS U29) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS U29),(OPS U29) #) is strict MSAlgebra over S
U2 is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S
U19 is Element of I
A . U19 is non empty set
EqR . U19 is set
U2 . U19 is non-empty MSAlgebra over S
U1 is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S
U2 is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S
U19 is set
U29 is Element of I
A . U29 is non empty set
EqR . U29 is set
U1 . U29 is non-empty MSAlgebra over S
U2 . U29 is non-empty MSAlgebra over S
U1 . U19 is set
U2 . U19 is set
F is non empty set
s9 is non empty set
s is non empty Relation-like F -defined Function-like total MSAlgebra-Family of F,S
product s is strict non-empty MSAlgebra over S
SORTS s 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 s 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 s)), the ResultSort of S * (SORTS 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,(SORTS s)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS 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 * (SORTS s) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS s),(OPS s) #) is strict MSAlgebra over S
f is non empty Relation-like s9 -defined Function-like total MSAlgebra-Family of s9,S
product f is strict non-empty MSAlgebra over S
SORTS f is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS f 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 f)), the ResultSort of S * (SORTS f)
K186( the carrier of S,(SORTS f)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS f)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS f) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS f),(OPS f) #) is strict MSAlgebra over S
U1 is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S
U2 is non empty Relation-like I -defined Function-like total MSAlgebra-Family of I,S
I is non empty set
K11(I,I) is non empty Relation-like set
K10(K11(I,I)) is non empty set
S is non empty non void V68() ManySortedSign
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 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
EqR is Relation-like I -defined I -valued V12() V14() V19() total Element of K10(K11(I,I))
Class EqR is non empty with_non-empty_elements non empty-membered a_partition of I
id (Class EqR) is non empty Relation-like non-empty non empty-yielding Class EqR -defined Class EqR -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11((Class EqR),(Class EqR)))
K11((Class EqR),(Class EqR)) is non empty Relation-like set
K10(K11((Class EqR),(Class EqR))) is non empty set
(I,S,A,EqR) is non empty Relation-like Class EqR -defined Function-like total ( Class EqR, id (Class EqR),S)
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) is non empty Relation-like Class EqR -defined Function-like total MSAlgebra-Family of Class EqR,S
product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) is strict non-empty MSAlgebra over S
SORTS ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS ((Class EqR),S,(id (Class EqR)),(I,S,A,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 ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))), the ResultSort of S * (SORTS ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))
K186( the carrier of S,(SORTS ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))),(OPS ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) #) is strict MSAlgebra over S
the Sorts of (product A) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
K10(I) is non empty set
F is set
the Sorts of (product A) . F is set
the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . F is set
s is Element of the carrier of S
the Sorts of (product 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
s9 is set
f is Relation-like Function-like set
y is non empty Relation-like Class EqR -defined Function-like total set
Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s) is non empty Relation-like non-empty non empty-yielding Class EqR -defined Function-like total set
dom (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s)) is non empty Element of K10((Class EqR))
K10((Class EqR)) is non empty set
x is set
y . x is set
(Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s)) . x is set
(I,S,A,EqR) . x is set
A | x is Relation-like x -defined I -defined Function-like set
f9 is non empty Element of K10(I)
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9 is set
(Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s)) . f9 is set
A | f9 is Relation-like f9 -defined I -defined Function-like set
dom (A | f9) is Element of K10(f9)
K10(f9) is non empty set
dom A is non empty Element of K10(I)
(dom A) /\ f9 is Element of K10(I)
I /\ f9 is Element of K10(I)
e is non empty Relation-like f9 -defined Function-like total set
e is set
e . e is set
A . e is set
f | f9 is Relation-like Function-like set
(Carrier (A,s)) | f9 is Relation-like f9 -defined I -defined Function-like set
product ((Carrier (A,s)) | f9) is functional with_common_domain product-like set
e is non empty Relation-like f9 -defined Function-like total MSAlgebra-Family of f9,S
Carrier (e,s) is non empty Relation-like non-empty non empty-yielding f9 -defined Function-like total set
product (Carrier (e,s)) is non empty functional with_common_domain product-like set
(id (Class EqR)) . f9 is set
(I,S,A,EqR) . f9 is set
Ji is non empty set
Cs is non empty Relation-like Ji -defined Function-like total MSAlgebra-Family of Ji,S
product Cs is strict non-empty MSAlgebra over S
SORTS Cs is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS Cs 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 Cs)), the ResultSort of S * (SORTS Cs)
K186( the carrier of S,(SORTS Cs)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS Cs)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS Cs) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS Cs),(OPS Cs) #) is strict MSAlgebra over S
y9 is MSAlgebra over S
the Sorts of y9 is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of y9 . s is set
dom y is non empty Element of K10((Class EqR))
product (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s)) is non empty functional with_common_domain product-like set
x is Relation-like Function-like set
x is Relation-like Function-like set
f9 is non empty Element of Class EqR
x . f9 is set
x | f9 is Relation-like Function-like set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V54() ManySortedFunction of the Sorts of (product A), the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))
s is Element of the carrier' of S
Args (s,(product A)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product A))
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_result_sort_of s is Element of the carrier of S
F . (the_result_sort_of s) is Relation-like the Sorts of (product A) . (the_result_sort_of s) -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s) -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . (the_result_sort_of s)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s))))
the Sorts of (product A) . (the_result_sort_of s) is non empty set
the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s) is non empty set
K11(( the Sorts of (product A) . (the_result_sort_of s)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s))) is non empty Relation-like set
K10(K11(( the Sorts of (product A) . (the_result_sort_of s)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s)))) is non empty set
Den (s,(product A)) is Relation-like Args (s,(product A)) -defined Result (s,(product A)) -valued Function-like quasi_total Element of K10(K11((Args (s,(product A))),(Result (s,(product A)))))
Result (s,(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 (s,(product A))),(Result (s,(product A)))) is non empty Relation-like set
K10(K11((Args (s,(product A))),(Result (s,(product A))))) is non empty set
Den (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) is Relation-like Args (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) -defined Result (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) -valued Function-like quasi_total Element of K10(K11((Args (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))),(Result (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))))))
Args (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))
K186( the carrier of S, the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) is set
Result (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))) is non empty Element of rng the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))
rng the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))),(Result (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)))))) is non empty Relation-like set
K10(K11((Args (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))),(Result (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))))) is non empty set
s9 is Relation-like Function-like Element of Args (s,(product A))
(Den (s,(product A))) . s9 is set
(F . (the_result_sort_of s)) . ((Den (s,(product A))) . s9) is set
F # s9 is Relation-like Function-like Element of Args (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))
(Den (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))) . (F # s9) is set
(Den (s,(product A))) . s9 is Element of Result (s,(product A))
(F . (the_result_sort_of s)) . ((Den (s,(product A))) . s9) is set
(Den (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))) . (F # s9) is Element of Result (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))
Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),(the_result_sort_of s)) is non empty Relation-like non-empty non empty-yielding Class EqR -defined Function-like total set
product (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),(the_result_sort_of s))) is non empty functional with_common_domain product-like set
dom (F . (the_result_sort_of s)) is Element of K10(( the Sorts of (product A) . (the_result_sort_of s)))
K10(( the Sorts of (product A) . (the_result_sort_of s))) is non empty set
(SORTS A) . (the_result_sort_of s) is non empty set
Carrier (A,(the_result_sort_of s)) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,(the_result_sort_of s))) is non empty functional with_common_domain product-like set
the_arity_of s 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),s) is Relation-like Function-like set
(Den (s,(product A))) . {} is set
(F . (the_result_sort_of s)) . (S,(product A),s) is set
rng (F . (the_result_sort_of s)) is Element of K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s)))
K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s))) is non empty set
dom (S,(product A),s) is set
dom (Carrier (A,(the_result_sort_of s))) is non empty Element of K10(I)
x is non empty Element of Class EqR
(id (Class EqR)) . x is non empty set
(I,S,A,EqR) . x is set
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x is non-empty MSAlgebra over S
f9 is non empty set
e is non empty Relation-like f9 -defined Function-like total MSAlgebra-Family of f9,S
product e is strict non-empty MSAlgebra over S
SORTS e is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS e 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 e)), the ResultSort of S * (SORTS e)
K186( the carrier of S,(SORTS e)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS e)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS e) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS e),(OPS e) #) is strict MSAlgebra over S
(S,(product A),s) | x is Relation-like Function-like set
dom ((S,(product A),s) | x) is set
I /\ x is Element of K10(I)
A | x is Relation-like x -defined I -defined Function-like set
dom (A | x) is Element of K10(x)
K10(x) is non empty set
dom A is non empty Element of K10(I)
(dom A) /\ x is Element of K10(I)
e is set
Ji is Element of f9
e . Ji is non-empty MSAlgebra over S
Cs is Element of I
A . Cs is non-empty MSAlgebra over S
((S,(product A),s) | x) . e is set
(S,(product A),s) . e is set
(S,(A . Cs),s) is set
Den (s,(A . Cs)) is Relation-like Args (s,(A . Cs)) -defined Result (s,(A . Cs)) -valued Function-like quasi_total Element of K10(K11((Args (s,(A . Cs))),(Result (s,(A . Cs)))))
Args (s,(A . Cs)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . Cs))
the Sorts of (A . Cs) 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 . Cs)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (A . Cs)) is set
Result (s,(A . Cs)) is non empty Element of rng the Sorts of (A . Cs)
rng the Sorts of (A . Cs) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(A . Cs))),(Result (s,(A . Cs)))) is non empty Relation-like set
K10(K11((Args (s,(A . Cs))),(Result (s,(A . Cs))))) is non empty set
(Den (s,(A . Cs))) . {} is set
(S,(product e),s) is Relation-like Function-like set
Den (s,(product e)) is Relation-like Args (s,(product e)) -defined Result (s,(product e)) -valued Function-like quasi_total Element of K10(K11((Args (s,(product e))),(Result (s,(product e)))))
Args (s,(product e)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product e))
the Sorts of (product e) 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 e)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (product e)) is set
Result (s,(product e)) is non empty Element of rng the Sorts of (product e)
rng the Sorts of (product e) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(product e))),(Result (s,(product e)))) is non empty Relation-like set
K10(K11((Args (s,(product e))),(Result (s,(product e))))) is non empty set
(Den (s,(product e))) . {} is set
(S,(product e),s) . e is set
{ (Result (s,(e . b₁))) where b₁ is Element of f9 : verum } is set
union { (Result (s,(e . b₁))) where b₁ is Element of f9 : verum } is set
Funcs (f9,(union { (Result (s,(e . b₁))) where b₁ is Element of f9 : verum } )) is set
dom (S,(product e),s) is set
(S,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x),s) is set
Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)) is Relation-like Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)) -defined Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)) -valued Function-like quasi_total Element of K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)))))
Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x))
the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x) 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 (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)) is set
Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)) is non empty Element of rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)
rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x)))) is non empty Relation-like set
K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x))))) is non empty set
(Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . x))) . {} is set
f9 is Relation-like Function-like set
x is set
x is Relation-like Function-like set
e is non empty Element of Class EqR
x . e is set
f9 | e is Relation-like Function-like set
e is Relation-like the Sorts of (product A) . (the_result_sort_of s) -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s) -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . (the_result_sort_of s)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s))))
x . x is set
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e is non-empty MSAlgebra over S
(S,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e),s) is set
Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is Relation-like Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) -defined Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) -valued Function-like quasi_total Element of K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)))))
Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))
the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e) 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 (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is set
Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is non empty Element of rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)
rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)))) is non empty Relation-like set
K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))))) is non empty set
(Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))) . {} is set
(S,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))),s) is Relation-like Function-like set
(Den (s,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))))) . {} is set
(S,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))),s) . x is set
{ (Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . b₁))) where b₁ is non empty Element of Class EqR : verum } is set
union { (Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . b₁))) where b₁ is non empty Element of Class EqR : verum } is set
Funcs ((Class EqR),(union { (Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . b₁))) where b₁ is non empty Element of Class EqR : verum } )) is set
dom (S,(product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))),s) is set
dom x is set
dom (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),(the_result_sort_of s))) is non empty Element of K10((Class EqR))
K10((Class EqR)) is non empty set
the_arity_of s is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))
x is Relation-like Function-like set
dom x is set
dom (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),(the_result_sort_of s))) is non empty Element of K10((Class EqR))
K10((Class EqR)) is non empty set
rng (F . (the_result_sort_of s)) is Element of K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s)))
K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s))) is non empty set
f9 is non empty Element of Class EqR
(id (Class EqR)) . f9 is non empty set
(I,S,A,EqR) . f9 is set
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9 is non-empty MSAlgebra over S
e is non empty set
e is non empty Relation-like e -defined Function-like total MSAlgebra-Family of e,S
product e is strict non-empty MSAlgebra over S
SORTS e is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS e 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 e)), the ResultSort of S * (SORTS e)
K186( the carrier of S,(SORTS e)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS e)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS e) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS e),(OPS e) #) is strict MSAlgebra over S
commute (F # s9) is Relation-like Function-like Function-yielding V54() set
(commute (F # s9)) . f9 is Relation-like Function-like set
Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9))
the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9) 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 (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)) is set
Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)) is Relation-like Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)) -defined Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)) -valued Function-like quasi_total Element of K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)))))
Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)) is non empty Element of rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)
rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9)))) is non empty Relation-like set
K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9))))) is non empty set
(Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9))) . ((commute (F # s9)) . f9) is set
Carrier (e,(the_result_sort_of s)) is non empty Relation-like non-empty non empty-yielding e -defined Function-like total set
product (Carrier (e,(the_result_sort_of s))) is non empty functional with_common_domain product-like set
Cs is Element of I
i is set
dom (the_arity_of s) is countable Element of K10(K160())
(the_arity_of s) . i is set
rng (the_arity_of s) is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
s9 . i is set
(the_arity_of s) /. i is Element of the carrier of S
Carrier (A,((the_arity_of s) /. i)) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,((the_arity_of s) /. i))) is non empty functional with_common_domain product-like set
e1 is Element of the carrier of S
Carrier (A,e1) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,e1)) is non empty functional with_common_domain product-like set
(SORTS A) . e1 is non empty set
f1 is Relation-like Function-like set
dom f1 is set
dom (Carrier (A,e1)) is non empty Element of K10(I)
f1 | f9 is Relation-like Function-like set
dom (f1 | f9) is set
I /\ f9 is Element of K10(I)
(F # s9) . i is set
Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),((the_arity_of s) /. i)) is non empty Relation-like non-empty non empty-yielding Class EqR -defined Function-like total set
product (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),((the_arity_of s) /. i))) is non empty functional with_common_domain product-like set
the Sorts of (product A) . e1 is non empty set
the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . e1 is non empty set
K11(( the Sorts of (product A) . e1),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . e1)) is non empty Relation-like set
K10(K11(( the Sorts of (product A) . e1),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . e1))) is non empty set
F . e1 is Relation-like the Sorts of (product A) . e1 -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . e1 -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . e1),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . e1)))
f7 is Relation-like the Sorts of (product A) . e1 -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . e1 -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . e1),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . e1)))
f5 is Relation-like Function-like set
F . ((the_arity_of s) /. i) is Relation-like the Sorts of (product A) . ((the_arity_of s) /. i) -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . ((the_arity_of s) /. i) -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . ((the_arity_of s) /. i)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . ((the_arity_of s) /. i))))
the Sorts of (product A) . ((the_arity_of s) /. i) is non empty set
the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . ((the_arity_of s) /. i) is non empty set
K11(( the Sorts of (product A) . ((the_arity_of s) /. i)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . ((the_arity_of s) /. i))) is non empty Relation-like set
K10(K11(( the Sorts of (product A) . ((the_arity_of s) /. i)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . ((the_arity_of s) /. i)))) is non empty set
(F . ((the_arity_of s) /. i)) . (s9 . i) is set
f7 . (s9 . i) is set
f5 . f9 is set
f6 is Relation-like Function-like set
((commute (F # s9)) . f9) . i is set
commute ((commute (F # s9)) . f9) is Relation-like Function-like Function-yielding V54() set
(commute ((commute (F # s9)) . f9)) . Cs is Relation-like Function-like set
((commute ((commute (F # s9)) . f9)) . Cs) . i is set
y9 is Element of e
(f1 | f9) . y9 is set
f1 . y9 is set
commute s9 is Relation-like Function-like Function-yielding V54() set
(commute s9) . Cs is Relation-like Function-like set
((commute s9) . Cs) . i is set
A . Cs is non-empty MSAlgebra over S
Args (s,(A . Cs)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . Cs))
the Sorts of (A . Cs) 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 . Cs)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (A . Cs)) is set
(the_arity_of s) * the Sorts of (A . Cs) is Relation-like non-empty K160() -defined Function-like set
product ((the_arity_of s) * the Sorts of (A . Cs)) is non empty functional with_common_domain product-like set
dom ((commute s9) . Cs) is set
dom ((the_arity_of s) * the Sorts of (A . Cs)) is countable Element of K10(K160())
(commute ((commute (F # s9)) . f9)) . y9 is Relation-like Function-like set
e . y9 is non-empty MSAlgebra over S
Args (s,(e . y9)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (e . y9))
the Sorts of (e . y9) 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 (e . y9)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (e . y9)) is set
(the_arity_of s) * the Sorts of (e . y9) is Relation-like non-empty K160() -defined Function-like set
product ((the_arity_of s) * the Sorts of (e . y9)) is non empty functional with_common_domain product-like set
dom ((commute ((commute (F # s9)) . f9)) . Cs) is set
dom ((the_arity_of s) * the Sorts of (e . y9)) is countable Element of K10(K160())
Cs is Relation-like Function-like set
dom Cs is set
dom (Carrier (A,(the_result_sort_of s))) is non empty Element of K10(I)
Cs | f9 is Relation-like Function-like set
dom (Cs | f9) is set
Args (s,(product e)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (product e))
the Sorts of (product e) 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 e)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (product e)) is set
A | f9 is Relation-like f9 -defined I -defined Function-like set
dom (A | f9) is Element of K10(f9)
K10(f9) is non empty set
dom A is non empty Element of K10(I)
(dom A) /\ f9 is Element of K10(I)
y9 is set
i is Element of e
e . i is non-empty MSAlgebra over S
e1 is Element of I
A . e1 is non-empty MSAlgebra over S
Ji is Relation-like Function-like set
Ji . y9 is set
Den (s,(A . e1)) is Relation-like Args (s,(A . e1)) -defined Result (s,(A . e1)) -valued Function-like quasi_total Element of K10(K11((Args (s,(A . e1))),(Result (s,(A . e1)))))
Args (s,(A . e1)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (A . e1))
the Sorts of (A . e1) 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 . e1)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (A . e1)) is set
Result (s,(A . e1)) is non empty Element of rng the Sorts of (A . e1)
rng the Sorts of (A . e1) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(A . e1))),(Result (s,(A . e1)))) is non empty Relation-like set
K10(K11((Args (s,(A . e1))),(Result (s,(A . e1))))) is non empty set
(commute ((commute (F # s9)) . f9)) . i is Relation-like Function-like set
(Den (s,(A . e1))) . ((commute ((commute (F # s9)) . f9)) . i) is set
(commute s9) . e1 is Relation-like Function-like set
(Den (s,(A . e1))) . ((commute s9) . e1) is set
Cs . y9 is set
(Cs | f9) . y9 is set
dom Ji is set
dom (Carrier (e,(the_result_sort_of s))) is non empty Element of K10(e)
K10(e) is non empty set
e is set
x is Relation-like Function-like set
e is non empty Element of Class EqR
x . e is set
f9 is Relation-like Function-like set
f9 | e is Relation-like Function-like set
Ji is Relation-like the Sorts of (product A) . (the_result_sort_of s) -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s) -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . (the_result_sort_of s)),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . (the_result_sort_of s))))
x . e is set
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e is non-empty MSAlgebra over S
Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is Relation-like Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) -defined Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) -valued Function-like quasi_total Element of K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)))))
Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is non empty functional Element of rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))
the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e) 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 (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is Relation-like K183( the carrier of S) -defined Function-like total set
rng K186( the carrier of S, the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is set
Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)) is non empty Element of rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)
rng the Sorts of (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e) is non empty with_non-empty_elements non empty-membered set
K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e)))) is non empty Relation-like set
K10(K11((Args (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))),(Result (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))))) is non empty set
(commute (F # s9)) . e is Relation-like Function-like set
(Den (s,(((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e))) . ((commute (F # s9)) . e) is set
x . e is set
dom x is set
the_arity_of s is Relation-like K160() -defined the carrier of S -valued Function-like V70() M11( the carrier of S,K183( the carrier of S))
s is set
dom F is non empty set
F . s is Relation-like Function-like set
s9 is Relation-like Function-like set
dom F is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the Sorts of (product A) . s is set
the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s is set
K11(( the Sorts of (product A) . s),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s)) is Relation-like set
K10(K11(( the Sorts of (product A) . s),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s))) is non empty set
f is Relation-like the Sorts of (product A) . s -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s)))
y is set
dom s9 is set
x is set
s9 . y is set
s9 . x is set
dom f is Element of K10(( the Sorts of (product A) . s))
K10(( the Sorts of (product A) . s)) is non empty set
x is Element of the carrier of S
the Sorts of (product A) . x is non empty set
Carrier (A,x) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,x)) is non empty functional with_common_domain product-like set
dom (Carrier (A,x)) is non empty Element of K10(I)
f9 is Relation-like Function-like set
dom f9 is set
e is Relation-like Function-like set
dom e is set
Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),x) is non empty Relation-like non-empty non empty-yielding Class EqR -defined Function-like total set
product (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),x)) is non empty functional with_common_domain product-like set
e is Relation-like Function-like set
f . f9 is set
Ji is set
e . Ji is set
f9 . Ji is set
Class (EqR,Ji) is Element of K10(I)
e | (Class (EqR,Ji)) is Relation-like Function-like set
e is Relation-like Function-like set
e . (Class (EqR,Ji)) is set
f9 | (Class (EqR,Ji)) is Relation-like Function-like set
(f9 | (Class (EqR,Ji))) . Ji is set
dom e is set
e is Relation-like Function-like set
dom e is set
s is set
F . s is Relation-like Function-like set
rng (F . s) is set
the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s is set
the Sorts of (product A) . s is set
K11(( the Sorts of (product A) . s),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s)) is Relation-like set
K10(K11(( the Sorts of (product A) . s),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s))) is non empty set
f is Relation-like the Sorts of (product A) . s -defined the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s -valued Function-like quasi_total Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s)))
s9 is Element of the carrier of S
the Sorts of (product A) . s9 is non empty set
Carrier (A,s9) is non empty Relation-like non-empty non empty-yielding I -defined Function-like total set
product (Carrier (A,s9)) is non empty functional with_common_domain product-like set
dom f is Element of K10(( the Sorts of (product A) . s))
K10(( the Sorts of (product A) . s)) is non empty set
y is set
Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s9) is non empty Relation-like non-empty non empty-yielding Class EqR -defined Function-like total set
product (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s9)) is non empty functional with_common_domain product-like set
dom (Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s9)) is non empty Element of K10((Class EqR))
K10((Class EqR)) is non empty set
x is Relation-like Function-like set
x is set
Class (EqR,x) is Element of K10(I)
f9 is non empty Element of Class EqR
(id (Class EqR)) . f9 is non empty set
(I,S,A,EqR) . f9 is set
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . f9 is non-empty MSAlgebra over S
e is non empty set
e is non empty Relation-like e -defined Function-like total MSAlgebra-Family of e,S
product e is strict non-empty MSAlgebra over S
SORTS e is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS e 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 e)), the ResultSort of S * (SORTS e)
K186( the carrier of S,(SORTS e)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS e)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS e) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS e),(OPS e) #) is strict MSAlgebra over S
(Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s9)) . f9 is non empty set
Carrier (e,s9) is non empty Relation-like non-empty non empty-yielding e -defined Function-like total set
product (Carrier (e,s9)) is non empty functional with_common_domain product-like set
Ji is MSAlgebra over S
the Sorts of Ji is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of Ji . s9 is set
x . f9 is set
Cs is Relation-like Function-like set
dom Cs is set
Ji is Relation-like Function-like set
Ji . x is set
Cs is non empty Element of Class EqR
y9 is Relation-like Function-like set
x . Cs is set
y9 . x is set
x is non empty Relation-like I -defined Function-like total set
dom (Carrier (A,s9)) is non empty Element of K10(I)
f9 is set
x . f9 is set
(Carrier (A,s9)) . f9 is set
e is non empty Element of Class EqR
e is Relation-like Function-like set
x . e is set
e . f9 is set
(Carrier (A,s9)) | e is Relation-like e -defined I -defined Function-like set
dom ((Carrier (A,s9)) | e) is Element of K10(e)
K10(e) is non empty set
(dom (Carrier (A,s9))) /\ e is Element of K10(I)
I /\ e is Element of K10(I)
((Carrier (A,s9)) | e) . f9 is set
(id (Class EqR)) . e is non empty set
(I,S,A,EqR) . e is set
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e is non-empty MSAlgebra over S
Ji is non empty set
Cs is non empty Relation-like Ji -defined Function-like total MSAlgebra-Family of Ji,S
product Cs is strict non-empty MSAlgebra over S
SORTS Cs is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS Cs 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 Cs)), the ResultSort of S * (SORTS Cs)
K186( the carrier of S,(SORTS Cs)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS Cs)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS Cs) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS Cs),(OPS Cs) #) is strict MSAlgebra over S
A | e is Relation-like e -defined I -defined Function-like set
Carrier (Cs,s9) is non empty Relation-like non-empty non empty-yielding Ji -defined Function-like total set
(Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s9)) . e is non empty set
product (Carrier (Cs,s9)) is non empty functional with_common_domain product-like set
y9 is MSAlgebra over S
the Sorts of y9 is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of y9 . s9 is set
y9 is Relation-like Function-like set
dom y9 is set
dom (Carrier (Cs,s9)) is non empty Element of K10(Ji)
K10(Ji) is non empty set
y9 is Relation-like Function-like set
dom y9 is set
dom x is non empty Element of K10(I)
f . x is set
rng f is Element of K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s))
K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s)) is non empty set
f9 is Relation-like Function-like set
e is set
x . e is set
f9 . e is set
e is non empty Element of Class EqR
(id (Class EqR)) . e is non empty set
(I,S,A,EqR) . e is set
((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)) . e is non-empty MSAlgebra over S
Ji is non empty set
Cs is non empty Relation-like Ji -defined Function-like total MSAlgebra-Family of Ji,S
product Cs is strict non-empty MSAlgebra over S
SORTS Cs is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
OPS Cs 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 Cs)), the ResultSort of S * (SORTS Cs)
K186( the carrier of S,(SORTS Cs)) is Relation-like K183( the carrier of S) -defined Function-like total set
the Arity of S * K186( the carrier of S,(SORTS Cs)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (SORTS Cs) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (SORTS Cs),(OPS Cs) #) is strict MSAlgebra over S
(Carrier (((Class EqR),S,(id (Class EqR)),(I,S,A,EqR)),s9)) . e is non empty set
Carrier (Cs,s9) is non empty Relation-like non-empty non empty-yielding Ji -defined Function-like total set
product (Carrier (Cs,s9)) is non empty functional with_common_domain product-like set
y9 is MSAlgebra over S
the Sorts of y9 is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of y9 . s9 is set
x . e is set
y9 is Relation-like Function-like set
dom y9 is set
x | e is Relation-like e -defined I -defined Function-like set
dom (x | e) is Element of K10(e)
K10(e) is non empty set
(dom x) /\ e is Element of K10(I)
I /\ e is Element of K10(I)
y9 is Relation-like Function-like set
i is set
(x | e) . i is set
y9 . i is set
x . i is set
e1 is non empty Element of Class EqR
f1 is Relation-like Function-like set
x . e1 is set
f1 . i is set
dom (Carrier (Cs,s9)) is non empty Element of K10(Ji)
K10(Ji) is non empty set
dom y9 is set
i is Relation-like Function-like set
dom i is set
e is Relation-like Function-like set
dom e is set
e is Relation-like Function-like set
dom e is set
x is set
f . x is set
rng f is Element of K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s))
K10(( the Sorts of (product ((Class EqR),S,(id (Class EqR)),(I,S,A,EqR))) . s)) is non empty set
x is set
f . x is set
x is set
f . x is set