:: UNIALG_3 semantic presentation

NAT is non empty V27() V28() V29() V34() V39() V40() Element of K19(REAL)

REAL is set

K19(REAL) is non empty set

NAT is non empty V27() V28() V29() V34() V39() V40() set

K19(NAT) is non empty V34() set

K19(NAT) is non empty V34() set

K279() is set

{} is functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered set

the functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered set is functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered set

1 is non empty set

2 is non empty set

3 is non empty set

0 is functional empty V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered Element of NAT

U0 is non empty V108() V109() non-empty UAStr

F is set

U0 is non empty V108() V109() non-empty UAStr

the non empty V108() V109() non-empty SubAlgebra of U0 is non empty V108() V109() non-empty SubAlgebra of U0

{ the non empty V108() V109() non-empty SubAlgebra of U0} is non empty trivial V41(1) set

a is set

a is (U0)

U0 is non empty V108() V109() non-empty UAStr

Sub U0 is non empty set

F is set

F is non empty (U0)

a is Element of F

U0 is non empty V108() V109() non-empty UAStr

(U0) is non empty (U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

F is non empty V108() V109() non-empty (U0,(U0))

a is non empty V108() V109() non-empty SubAlgebra of U0

the carrier of a is non empty set

a is Element of K19( the carrier of U0)

H1 is non empty V108() V109() non-empty SubAlgebra of U0

a is Element of K19( the carrier of U0)

the carrier of H1 is non empty set

a1 is non empty V108() V109() non-empty SubAlgebra of U0

a is Element of K19( the carrier of U0)

the carrier of a1 is non empty set

U0 is non empty V108() V109() non-empty UAStr

(U0) is non empty (U0)

the carrier of U0 is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

F is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

F is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

a is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

a is set

F . a is set

a . a is set

H1 is non empty V108() V109() non-empty (U0,(U0))

(U0,H1) is Element of K19( the carrier of U0)

a1 is non empty V108() V109() non-empty SubAlgebra of U0

the carrier of a1 is non empty set

F . H1 is Element of bool the carrier of U0

U0 is non empty V108() V109() non-empty UAStr

(U0) is non empty (U0)

F is set

a is non empty strict V108() V109() non-empty SubAlgebra of U0

U0 is non empty V108() V109() non-empty UAStr

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

F is non empty Element of K19( the carrier of U0)

a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

arity a is V27() V28() V29() V33() V34() V39() Element of NAT

a . {} is set

a is Relation-like NAT -defined F -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of F

len a is V27() V28() V29() V33() V34() V39() Element of NAT

a is Relation-like NAT -defined F -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of F

len a is V27() V28() V29() V33() V34() V39() Element of NAT

a . a is set

U0 is non empty V108() V109() non-empty UAStr

the carrier of U0 is non empty set

F is non empty V108() V109() non-empty SubAlgebra of U0

the carrier of F is non empty set

K19( the carrier of U0) is non empty set

U0 is non empty V108() V109() non-empty UAStr

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

F is non empty Element of K19( the carrier of U0)

a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

arity a is V27() V28() V29() V33() V34() V39() Element of NAT

a /. F is Relation-like F * -defined F -valued Function-like non empty homogeneous V119(F) Element of K19(K20((F *),F))

F * is functional non empty FinSequence-membered FinSequenceSet of F

K20((F *),F) is non empty set

K19(K20((F *),F)) is non empty set

dom a is functional FinSequence-membered Element of K19(( the carrier of U0 *))

K19(( the carrier of U0 *)) is non empty set

0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0

<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0

K20(NAT, the carrier of U0) is non empty V34() set

{(<*> the carrier of U0)} is non empty trivial V41(1) set

<*> F is Relation-like NAT -defined F -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of F

K20(NAT,F) is non empty V34() set

{(<*> F)} is non empty trivial V41(1) set

0 -tuples_on F is FinSequenceSet of F

a | (0 -tuples_on F) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Element of K19(K20(( the carrier of U0 *), the carrier of U0))

K20(( the carrier of U0 *), the carrier of U0) is non empty set

K19(K20(( the carrier of U0 *), the carrier of U0)) is non empty set

U0 is non empty V108() V109() non-empty UAStr

Constants U0 is Element of K19( the carrier of U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

{ (b

a is set

a is Element of the carrier of U0

H1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

arity H1 is V27() V28() V29() V33() V34() V39() Element of NAT

rng H1 is Element of K19( the carrier of U0)

H1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

arity H1 is V27() V28() V29() V33() V34() V39() Element of NAT

rng H1 is Element of K19( the carrier of U0)

dom H1 is functional FinSequence-membered Element of K19(( the carrier of U0 *))

K19(( the carrier of U0 *)) is non empty set

a1 is set

H1 . a1 is set

0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0

K20(NAT, the carrier of U0) is non empty V34() set

U1 is Relation-like NAT -defined the carrier of U0 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of U0

len U1 is V27() V28() V29() V33() V34() V39() Element of NAT

a is set

a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

a . {} is set

arity a is V27() V28() V29() V33() V34() V39() Element of NAT

dom a is functional FinSequence-membered Element of K19(( the carrier of U0 *))

K19(( the carrier of U0 *)) is non empty set

0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0

<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0

K20(NAT, the carrier of U0) is non empty V34() set

{(<*> the carrier of U0)} is non empty trivial V41(1) set

{} the carrier of U0 is functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-membered Element of K19( the carrier of U0)

a . ({} the carrier of U0) is set

rng a is Element of K19( the carrier of U0)

U0 is non empty V108() V109() non-empty with_const_op UAStr

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

F is non empty V108() V109() non-empty SubAlgebra of U0

Constants F is Element of K19( the carrier of F)

the carrier of F is non empty set

K19( the carrier of F) is non empty set

the carrier of F * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F

Operations F is non empty PFuncsDomHQN of the carrier of F

the charact of F is Relation-like NAT -defined K36(( the carrier of F *), the carrier of F) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of F *), the carrier of F)

K36(( the carrier of F *), the carrier of F) is set

rng the charact of F is set

{ b

( arity b

a is set

H1 is Element of the carrier of U0

a1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT

rng a1 is Element of K19( the carrier of U0)

a1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT

rng a1 is Element of K19( the carrier of U0)

dom a1 is functional FinSequence-membered Element of K19(( the carrier of U0 *))

K19(( the carrier of U0 *)) is non empty set

0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0

<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0

K20(NAT, the carrier of U0) is non empty V34() set

{(<*> the carrier of U0)} is non empty trivial V41(1) set

a is non empty Element of K19( the carrier of U0)

<*> a is Relation-like NAT -defined a -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of a

K20(NAT,a) is non empty V34() set

{(<*> a)} is non empty trivial V41(1) set

0 -tuples_on a is FinSequenceSet of a

dom the charact of U0 is Element of K19(NAT)

U1 is set

the charact of U0 . U1 is set

H is V27() V28() V29() V33() V34() V39() Element of NAT

dom the charact of F is Element of K19(NAT)

the charact of F . H is set

Opers (U0,a) is Relation-like NAT -defined K36((a *),a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36((a *),a)

a * is functional non empty FinSequence-membered FinSequenceSet of a

K36((a *),a) is set

dom (Opers (U0,a)) is Element of K19(NAT)

(Opers (U0,a)) . H is set

a1 /. a is Relation-like a * -defined a -valued Function-like non empty homogeneous V119(a) Element of K19(K20((a *),a))

K20((a *),a) is non empty set

K19(K20((a *),a)) is non empty set

H1 is Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F

a1 | (0 -tuples_on a) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Element of K19(K20(( the carrier of U0 *), the carrier of U0))

K20(( the carrier of U0 *), the carrier of U0) is non empty set

K19(K20(( the carrier of U0 *), the carrier of U0)) is non empty set

a is set

H1 is Element of the carrier of F

a1 is Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F

arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT

rng a1 is Element of K19( the carrier of F)

a1 is Relation-like the carrier of F * -defined the carrier of F -valued Function-like non empty homogeneous V119( the carrier of F) Element of Operations F

arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT

rng a1 is Element of K19( the carrier of F)

dom the charact of F is Element of K19(NAT)

U1 is set

the charact of F . U1 is set

H is V27() V28() V29() V33() V34() V39() Element of NAT

dom the charact of U0 is Element of K19(NAT)

the charact of U0 . H is set

signature F is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature F) is V27() V28() V29() V33() V34() V39() Element of NAT

len the charact of F is V27() V28() V29() V33() V34() V39() Element of NAT

dom (signature F) is Element of K19(NAT)

signature U0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of NAT

H1 is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

arity H1 is V27() V28() V29() V33() V34() V39() Element of NAT

(signature F) . H is set

dom H1 is functional FinSequence-membered Element of K19(( the carrier of U0 *))

K19(( the carrier of U0 *)) is non empty set

0 -tuples_on the carrier of U0 is FinSequenceSet of the carrier of U0

<*> the carrier of U0 is Relation-like NAT -defined the carrier of U0 -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of U0

K20(NAT, the carrier of U0) is non empty V34() set

{(<*> the carrier of U0)} is non empty trivial V41(1) set

a is non empty Element of K19( the carrier of U0)

<*> a is Relation-like NAT -defined a -valued Function-like functional empty proper V27() V28() V29() V31() V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of a

K20(NAT,a) is non empty V34() set

{(<*> a)} is non empty trivial V41(1) set

0 -tuples_on a is FinSequenceSet of a

Opers (U0,a) is Relation-like NAT -defined K36((a *),a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36((a *),a)

a * is functional non empty FinSequence-membered FinSequenceSet of a

K36((a *),a) is set

dom (Opers (U0,a)) is Element of K19(NAT)

(Opers (U0,a)) . H is set

H1 /. a is Relation-like a * -defined a -valued Function-like non empty homogeneous V119(a) Element of K19(K20((a *),a))

K20((a *),a) is non empty set

K19(K20((a *),a)) is non empty set

H1 | (0 -tuples_on a) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Element of K19(K20(( the carrier of U0 *), the carrier of U0))

K20(( the carrier of U0 *), the carrier of U0) is non empty set

K19(K20(( the carrier of U0 *), the carrier of U0)) is non empty set

U0 is non empty V108() V109() non-empty with_const_op UAStr

F is non empty V108() V109() non-empty SubAlgebra of U0

a is non empty V108() V109() non-empty UAStr

Constants a is Element of K19( the carrier of a)

the carrier of a is non empty set

K19( the carrier of a) is non empty set

the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a

Operations a is non empty PFuncsDomHQN of the carrier of a

the charact of a is Relation-like NAT -defined K36(( the carrier of a *), the carrier of a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of a *), the carrier of a)

K36(( the carrier of a *), the carrier of a) is set

rng the charact of a is set

{ b

( arity b

the Element of Constants a is Element of Constants a

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

H1 is Element of the carrier of a

a1 is Relation-like the carrier of a * -defined the carrier of a -valued Function-like non empty homogeneous V119( the carrier of a) Element of Operations a

arity a1 is V27() V28() V29() V33() V34() V39() Element of NAT

rng a1 is Element of K19( the carrier of a)

U0 is non empty V108() V109() non-empty with_const_op UAStr

F is non empty V108() V109() non-empty with_const_op SubAlgebra of U0

Constants F is non empty Element of K19( the carrier of F)

the carrier of F is non empty set

K19( the carrier of F) is non empty set

the carrier of F * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F

Operations F is non empty PFuncsDomHQN of the carrier of F

the charact of F is Relation-like NAT -defined K36(( the carrier of F *), the carrier of F) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of F *), the carrier of F)

K36(( the carrier of F *), the carrier of F) is set

rng the charact of F is set

{ b

( arity b

a is non empty V108() V109() non-empty with_const_op SubAlgebra of U0

Constants a is non empty Element of K19( the carrier of a)

the carrier of a is non empty set

K19( the carrier of a) is non empty set

the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a

Operations a is non empty PFuncsDomHQN of the carrier of a

the charact of a is Relation-like NAT -defined K36(( the carrier of a *), the carrier of a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of a *), the carrier of a)

K36(( the carrier of a *), the carrier of a) is set

rng the charact of a is set

{ b

( arity b

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

U0 is non empty V108() V109() non-empty UAStr

(U0) is non empty (U0)

the carrier of U0 is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

F is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

a is non empty V108() V109() non-empty (U0,(U0))

a is non empty V108() V109() non-empty SubAlgebra of U0

(U0,a) is Element of K19( the carrier of U0)

F . a is Element of bool the carrier of U0

the carrier of a is non empty set

H1 is non empty V108() V109() non-empty SubAlgebra of U0

the carrier of H1 is non empty set

a is non empty V108() V109() non-empty (U0,(U0))

F . a is Element of bool the carrier of U0

(U0,a) is Element of K19( the carrier of U0)

a is non empty V108() V109() non-empty (U0,(U0))

the carrier of a is non empty set

U0 is non empty V108() V109() non-empty UAStr

the carrier of U0 is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

(U0) is non empty (U0)

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

F is non empty strict V108() V109() non-empty SubAlgebra of U0

(U0) . F is set

a is Element of the carrier of U0

the carrier of F is non empty set

the carrier of F is non empty set

U0 is non empty V108() V109() non-empty UAStr

(U0) is non empty (U0)

K19((U0)) is non empty set

the carrier of U0 is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

F is non empty Element of K19((U0))

(U0) .: F is Element of K19((bool the carrier of U0))

K19((bool the carrier of U0)) is non empty set

a is non empty V108() V109() non-empty (U0,(U0))

(U0) . a is Element of bool the carrier of U0

U0 is non empty V108() V109() non-empty with_const_op UAStr

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

(U0) is non empty (U0)

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19(K19( the carrier of U0)) is non empty set

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

(U0) . F is set

the carrier of F is non empty set

Constants F is non empty Element of K19( the carrier of F)

K19( the carrier of F) is non empty set

the carrier of F * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F

Operations F is non empty PFuncsDomHQN of the carrier of F

the charact of F is Relation-like NAT -defined K36(( the carrier of F *), the carrier of F) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of F *), the carrier of F)

K36(( the carrier of F *), the carrier of F) is set

rng the charact of F is set

{ b

( arity b

U0 is non empty V108() V109() non-empty with_const_op UAStr

the carrier of U0 is non empty set

Constants U0 is non empty Element of K19( the carrier of U0)

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

F is non empty V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of F is non empty set

a is set

K19( the carrier of F) is non empty set

U0 is non empty V108() V109() non-empty with_const_op UAStr

(U0) is non empty (U0)

K19((U0)) is non empty set

the carrier of U0 is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

F is non empty Element of K19((U0))

(U0) .: F is Element of K19((bool the carrier of U0))

K19((bool the carrier of U0)) is non empty set

meet ((U0) .: F) is Element of K19( the carrier of U0)

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

the Element of Constants U0 is Element of Constants U0

H1 is set

a1 is Element of K19( the carrier of U0)

U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))

(U0) . U1 is Element of bool the carrier of U0

H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of H is non empty set

a is Element of K19(K19( the carrier of U0))

U0 is non empty V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

the carrier of (UnSubAlLattice U0) is non empty set

(U0) is non empty (U0)

U0 is non empty V108() V109() non-empty with_const_op UAStr

(U0) is non empty (U0)

K19((U0)) is non empty set

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19(K19( the carrier of U0)) is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

F is non empty Element of K19((U0))

(U0) .: F is Element of K19((bool the carrier of U0))

K19((bool the carrier of U0)) is non empty set

meet ((U0) .: F) is Element of K19( the carrier of U0)

a is non empty Element of K19( the carrier of U0)

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

a is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous V119( the carrier of U0) Element of Operations U0

H1 is Relation-like NAT -defined a -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of a

len H1 is V27() V28() V29() V33() V34() V39() Element of NAT

arity a is V27() V28() V29() V33() V34() V39() Element of NAT

a . H1 is set

a1 is set

U1 is Element of K19( the carrier of U0)

H is non empty V108() V109() non-empty with_const_op (U0,(U0))

(U0) . H is Element of bool the carrier of U0

the carrier of H is non empty set

H1 is non empty Element of K19( the carrier of U0)

l4 is Relation-like NAT -defined H1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of H1

a . l4 is set

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

(U0) is non empty (U0)

K19((U0)) is non empty set

the carrier of U0 is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

F is non empty Element of K19((U0))

(U0) .: F is Element of K19((bool the carrier of U0))

K19((bool the carrier of U0)) is non empty set

meet ((U0) .: F) is Element of K19( the carrier of U0)

a is non empty Element of K19( the carrier of U0)

UniAlgSetClosed a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

Opers (U0,a) is Relation-like NAT -defined K36((a *),a) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36((a *),a)

a * is functional non empty FinSequence-membered FinSequenceSet of a

K36((a *),a) is set

UAStr(# a,(Opers (U0,a)) #) is strict UAStr

a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a is non empty set

a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a is non empty set

U0 is non empty V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

the carrier of (UnSubAlLattice U0) is non empty set

F is Element of the carrier of (UnSubAlLattice U0)

a is Element of the carrier of (UnSubAlLattice U0)

a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a is non empty set

the carrier of H1 is non empty set

a1 is Element of the carrier of (UnSubAlLattice U0)

U1 is Element of the carrier of (UnSubAlLattice U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

H1 is Element of K19( the carrier of U0)

H is Element of K19( the carrier of U0)

H1 \/ H is Element of K19( the carrier of U0)

a1 "\/" U1 is Element of the carrier of (UnSubAlLattice U0)

the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set

K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set

K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set

K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a1,U1) is Element of the carrier of (UnSubAlLattice U0)

a "\/" H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

l4 is non empty Element of K19( the carrier of U0)

GenUnivAlg l4 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a \/ the carrier of H1 is non empty set

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

H1 is Element of K19( the carrier of U0)

H is Element of K19( the carrier of U0)

H1 \/ H is Element of K19( the carrier of U0)

l4 is non empty Element of K19( the carrier of U0)

GenUnivAlg l4 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a "\/" H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a1 "\/" U1 is Element of the carrier of (UnSubAlLattice U0)

the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set

K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set

K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set

K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a1,U1) is Element of the carrier of (UnSubAlLattice U0)

U0 is non empty V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

the carrier of (UnSubAlLattice U0) is non empty set

F is Element of the carrier of (UnSubAlLattice U0)

a is Element of the carrier of (UnSubAlLattice U0)

a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a is non empty set

the carrier of H1 is non empty set

the carrier of a is non empty set

the carrier of H1 is non empty set

K19( the carrier of H1) is non empty set

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

GenUnivAlg (Constants U0) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of (UnSubAlLattice U0) is non empty set

a is Element of the carrier of (UnSubAlLattice U0)

H1 is Element of the carrier of (UnSubAlLattice U0)

a "/\" H1 is Element of the carrier of (UnSubAlLattice U0)

the L_meet of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set

K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set

K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set

K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),a,H1) is Element of the carrier of (UnSubAlLattice U0)

H1 "/\" a is Element of the carrier of (UnSubAlLattice U0)

K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),H1,a) is Element of the carrier of (UnSubAlLattice U0)

a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a1 is non empty set

F is Element of K19( the carrier of U0)

U1 is Element of K19( the carrier of U0)

F \/ U1 is Element of K19( the carrier of U0)

K19( the carrier of a1) is non empty set

H is non empty Element of K19( the carrier of U0)

GenUnivAlg H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a "\/" a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a "\/" H1 is Element of the carrier of (UnSubAlLattice U0)

the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))

K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a,H1) is Element of the carrier of (UnSubAlLattice U0)

a "/\" H1 is Element of the carrier of (UnSubAlLattice U0)

H1 "/\" a is Element of the carrier of (UnSubAlLattice U0)

the carrier of (UnSubAlLattice U0) is non empty set

F is Element of the carrier of (UnSubAlLattice U0)

a is Element of the carrier of (UnSubAlLattice U0)

F "\/" a is Element of the carrier of (UnSubAlLattice U0)

the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set

K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set

K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set

K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),F,a) is Element of the carrier of (UnSubAlLattice U0)

a "\/" F is Element of the carrier of (UnSubAlLattice U0)

K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a,F) is Element of the carrier of (UnSubAlLattice U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a is non empty set

H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of H1 is non empty set

a1 is Element of K19( the carrier of U0)

U1 is Element of K19( the carrier of U0)

a1 \/ U1 is Element of K19( the carrier of U0)

H is non empty Element of K19( the carrier of U0)

F "\/" a is Element of the carrier of (UnSubAlLattice U0)

a "\/" H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

[#] the carrier of a is non empty non proper Element of K19( the carrier of a)

K19( the carrier of a) is non empty set

GenUnivAlg ([#] the carrier of a) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of a

a "\/" F is Element of the carrier of (UnSubAlLattice U0)

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

GenUnivAlg (Constants U0) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

(GenUnivAlg (Constants U0)) /\ F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of F is non empty set

K19( the carrier of F) is non empty set

the carrier of (GenUnivAlg (Constants U0)) is non empty set

the carrier of ((GenUnivAlg (Constants U0)) /\ F) is non empty set

the carrier of (GenUnivAlg (Constants U0)) /\ the carrier of F is set

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

Bottom (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)

the carrier of (UnSubAlLattice U0) is non empty set

Constants U0 is non empty Element of K19( the carrier of U0)

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

the carrier of U0 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U0

Operations U0 is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is Relation-like NAT -defined K36(( the carrier of U0 *), the carrier of U0) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of K36(( the carrier of U0 *), the carrier of U0)

K36(( the carrier of U0 *), the carrier of U0) is set

rng the charact of U0 is set

{ b

( arity b

GenUnivAlg (Constants U0) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

(U0) is non empty (U0)

a is non empty V108() V109() non-empty with_const_op (U0,(U0))

a1 is Element of the carrier of (UnSubAlLattice U0)

U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))

H1 is Element of the carrier of (UnSubAlLattice U0)

H1 "/\" a1 is Element of the carrier of (UnSubAlLattice U0)

the L_meet of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set

K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set

K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set

K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),H1,a1) is Element of the carrier of (UnSubAlLattice U0)

H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

(GenUnivAlg (Constants U0)) /\ H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a1 "/\" H1 is Element of the carrier of (UnSubAlLattice U0)

K84( the carrier of (UnSubAlLattice U0), the L_meet of (UnSubAlLattice U0),a1,H1) is Element of the carrier of (UnSubAlLattice U0)

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

F is non empty V108() V109() non-empty with_const_op SubAlgebra of U0

a is Element of K19( the carrier of U0)

GenUnivAlg a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

(GenUnivAlg a) "\/" F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of F is non empty set

a \/ the carrier of F is non empty set

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

Top (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)

the carrier of (UnSubAlLattice U0) is non empty set

F is Element of K19( the carrier of U0)

GenUnivAlg F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

(U0) is non empty (U0)

a is non empty V108() V109() non-empty with_const_op (U0,(U0))

a1 is Element of the carrier of (UnSubAlLattice U0)

U1 is non empty V108() V109() non-empty with_const_op (U0,(U0))

H1 is Element of the carrier of (UnSubAlLattice U0)

H1 "\/" a1 is Element of the carrier of (UnSubAlLattice U0)

the L_join of (UnSubAlLattice U0) is Relation-like K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) Element of K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)))

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set

K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0)) is non empty set

K19(K20(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)), the carrier of (UnSubAlLattice U0))) is non empty set

K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),H1,a1) is Element of the carrier of (UnSubAlLattice U0)

H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

(GenUnivAlg F) "\/" H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a1 "\/" H1 is Element of the carrier of (UnSubAlLattice U0)

K84( the carrier of (UnSubAlLattice U0), the L_join of (UnSubAlLattice U0),a1,H1) is Element of the carrier of (UnSubAlLattice U0)

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

Top (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)

the carrier of (UnSubAlLattice U0) is non empty set

the carrier of U0 is non empty set

K19( the carrier of U0) is non empty set

F is Element of K19( the carrier of U0)

GenUnivAlg F is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

the carrier of (UnSubAlLattice U0) is non empty set

K19( the carrier of (UnSubAlLattice U0)) is non empty set

F is Element of K19( the carrier of (UnSubAlLattice U0))

Top (UnSubAlLattice U0) is Element of the carrier of (UnSubAlLattice U0)

a is Element of the carrier of (UnSubAlLattice U0)

a is Element of the carrier of (UnSubAlLattice U0)

(U0) is non empty (U0)

K19((U0)) is non empty set

a is non empty Element of K19((U0))

(U0,a) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

a is Element of the carrier of (UnSubAlLattice U0)

the Element of a is Element of a

a1 is Element of the carrier of (UnSubAlLattice U0)

the carrier of U0 is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

H is non empty V108() V109() non-empty with_const_op (U0,(U0))

(U0) . H is Element of bool the carrier of U0

U1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of U1 is non empty set

(U0) .: a is Element of K19((bool the carrier of U0))

K19((bool the carrier of U0)) is non empty set

meet ((U0) .: a) is Element of K19( the carrier of U0)

the carrier of (U0,a) is non empty set

a1 is Element of the carrier of (UnSubAlLattice U0)

the carrier of U0 is non empty set

bool the carrier of U0 is non empty Element of K19(K19( the carrier of U0))

K19( the carrier of U0) is non empty set

K19(K19( the carrier of U0)) is non empty set

(U0) is Relation-like (U0) -defined bool the carrier of U0 -valued Function-like V18((U0), bool the carrier of U0) Element of K19(K20((U0),(bool the carrier of U0)))

K20((U0),(bool the carrier of U0)) is non empty set

K19(K20((U0),(bool the carrier of U0))) is non empty set

(U0) .: a is Element of K19((bool the carrier of U0))

K19((bool the carrier of U0)) is non empty set

U1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of U1 is non empty set

H is set

H1 is Element of K19( the carrier of U0)

l4 is non empty V108() V109() non-empty with_const_op (U0,(U0))

(U0) . l4 is Element of bool the carrier of U0

l4 is Element of the carrier of (UnSubAlLattice U0)

U2 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of U2 is non empty set

(U0) . the Element of a is Element of bool the carrier of U0

(U0) .: F is Element of K19((bool the carrier of U0))

meet ((U0) .: a) is Element of K19( the carrier of U0)

the carrier of (U0,a) is non empty set

U0 is non empty V108() V109() non-empty with_const_op UAStr

the carrier of U0 is non empty set

F is non empty V108() V109() non-empty with_const_op UAStr

the carrier of F is non empty set

K20( the carrier of U0, the carrier of F) is non empty set

K19(K20( the carrier of U0, the carrier of F)) is non empty set

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

the carrier of (UnSubAlLattice U0) is non empty set

UnSubAlLattice F is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

Sub F is non empty set

UniAlg_join F is Relation-like K20((Sub F),(Sub F)) -defined Sub F -valued Function-like V18(K20((Sub F),(Sub F)), Sub F) Element of K19(K20(K20((Sub F),(Sub F)),(Sub F)))

K20((Sub F),(Sub F)) is non empty set

K20(K20((Sub F),(Sub F)),(Sub F)) is non empty set

K19(K20(K20((Sub F),(Sub F)),(Sub F))) is non empty set

UniAlg_meet F is Relation-like K20((Sub F),(Sub F)) -defined Sub F -valued Function-like V18(K20((Sub F),(Sub F)), Sub F) Element of K19(K20(K20((Sub F),(Sub F)),(Sub F)))

LattStr(# (Sub F),(UniAlg_join F),(UniAlg_meet F) #) is non empty strict LattStr

the carrier of (UnSubAlLattice F) is non empty set

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) is non empty set

K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F))) is non empty set

K19( the carrier of F) is non empty set

a is Relation-like the carrier of U0 -defined the carrier of F -valued Function-like V18( the carrier of U0, the carrier of F) Element of K19(K20( the carrier of U0, the carrier of F))

a is set

H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of H1 is non empty set

a .: the carrier of H1 is Element of K19( the carrier of F)

GenUnivAlg (a .: the carrier of H1) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F

a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F

U1 is Element of the carrier of (UnSubAlLattice F)

H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

H1 is Element of K19( the carrier of F)

the carrier of H is non empty set

a .: the carrier of H is Element of K19( the carrier of F)

GenUnivAlg (a .: the carrier of H) is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F

a is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice F) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)))

H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of H1 is non empty set

a .: the carrier of H1 is Element of K19( the carrier of F)

a . H1 is set

a1 is Element of K19( the carrier of F)

GenUnivAlg a1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F

(U0) is non empty (U0)

a is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice F) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)))

H1 is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice F) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice F)))

a1 is set

a . a1 is set

H1 . a1 is set

U1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of U1 is non empty set

a .: the carrier of U1 is Element of K19( the carrier of F)

H is Element of K19( the carrier of F)

GenUnivAlg H is non empty strict V108() V109() non-empty with_const_op SubAlgebra of F

U0 is non empty strict V108() V109() non-empty with_const_op UAStr

the carrier of U0 is non empty set

K20( the carrier of U0, the carrier of U0) is non empty set

K19(K20( the carrier of U0, the carrier of U0)) is non empty set

id the carrier of U0 is Relation-like non empty set

UnSubAlLattice U0 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr

Sub U0 is non empty set

UniAlg_join U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

K20((Sub U0),(Sub U0)) is non empty set

K20(K20((Sub U0),(Sub U0)),(Sub U0)) is non empty set

K19(K20(K20((Sub U0),(Sub U0)),(Sub U0))) is non empty set

UniAlg_meet U0 is Relation-like K20((Sub U0),(Sub U0)) -defined Sub U0 -valued Function-like V18(K20((Sub U0),(Sub U0)), Sub U0) Element of K19(K20(K20((Sub U0),(Sub U0)),(Sub U0)))

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is non empty strict LattStr

the carrier of (UnSubAlLattice U0) is non empty set

id the carrier of (UnSubAlLattice U0) is Relation-like non empty set

F is Relation-like the carrier of U0 -defined the carrier of U0 -valued Function-like V18( the carrier of U0, the carrier of U0) Element of K19(K20( the carrier of U0, the carrier of U0))

(U0,U0,F) is Relation-like the carrier of (UnSubAlLattice U0) -defined the carrier of (UnSubAlLattice U0) -valued Function-like V18( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) Element of K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)))

K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0)) is non empty set

K19(K20( the carrier of (UnSubAlLattice U0), the carrier of (UnSubAlLattice U0))) is non empty set

a is set

(U0,U0,F) . a is set

a is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

the carrier of a is non empty set

F .: the carrier of a is Element of K19( the carrier of U0)

K19( the carrier of U0) is non empty set

H1 is set

a1 is Element of the carrier of U0

F . a1 is Element of the carrier of U0

H1 is set

a1 is Element of the carrier of U0

U1 is Element of the carrier of U0

F . U1 is Element of the carrier of U0

(U0,U0,F) . a is set

H1 is Element of K19( the carrier of U0)

GenUnivAlg H1 is non empty strict V108() V109() non-empty with_const_op SubAlgebra of U0

dom (U0,U0,F) is Element of K19( the carrier of (UnSubAlLattice U0))

K19( the carrier of (UnSubAlLattice U0)) is non empty set