:: HEYTING2 semantic presentation

K129() is set

bool K129() is non empty cup-closed diff-closed preBoolean set

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

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

1 is non empty set

union {} is finite set

{{}} is functional non empty finite V47() set

V is set

C is set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

v is set

u is set

{ b

( not b

( not b

r is finite Element of Fin (PFuncs (V,C))

V is set

C is set

u is set

C \/ u is set

V is set

C is set

PFuncs (V,C) is functional non empty set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is Relation-like Function-like finite Element of PFuncs (V,C)

{u} is functional non empty finite V47() set

v is Relation-like Function-like Element of PFuncs (V,C)

r is Relation-like Function-like Element of PFuncs (V,C)

v is set

{.u.} is functional non empty finite V47() Element of Fin (PFuncs (V,C))

{ b

( not b

( not b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

v is functional finite Element of SubstitutionSet (V,C)

u ^ v is finite Element of Fin (PFuncs (V,C))

r is set

v9 is set

w is set

v9 \/ w is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

v is functional finite Element of SubstitutionSet (V,C)

u ^ v is finite Element of Fin (PFuncs (V,C))

mi (u ^ v) is functional finite Element of SubstitutionSet (V,C)

r is set

v9 is set

w is set

v9 \/ w is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

v is functional finite Element of SubstitutionSet (V,C)

u ^ v is finite Element of Fin (PFuncs (V,C))

mi (u ^ v) is functional finite Element of SubstitutionSet (V,C)

r is set

v9 is set

w is set

v9 \/ w is set

pf is set

pf \/ v9 is set

a is Relation-like Function-like Element of PFuncs (V,C)

sf is Relation-like Function-like Element of PFuncs (V,C)

r is set

v9 is set

w is Relation-like Function-like Element of PFuncs (V,C)

pf is Relation-like Function-like Element of PFuncs (V,C)

mi u is functional finite Element of SubstitutionSet (V,C)

sf is finite set

a is set

SA is set

a \/ SA is set

w \/ pf is Relation-like set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

v is set

r is set

v9 is Relation-like Function-like finite set

dom v9 is finite set

w is Relation-like Function-like set

dom w is set

rng w is set

v is set

r is set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

(V,C,u) is set

v is set

r is Relation-like Function-like finite set

dom r is finite set

v9 is Relation-like Function-like set

dom v9 is set

rng v9 is set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is non empty finite Element of Fin (PFuncs (V,C))

(V,C,u) is set

{ H

r is set

v9 is Relation-like Function-like Element of PFuncs (V,C)

dom v9 is set

{ H

r is set

v9 is Relation-like Function-like finite set

dom v9 is finite set

v9 is set

w is Relation-like Function-like Element of PFuncs (V,C)

dom w is set

union { H

r is Relation-like Function-like Element of PFuncs (V,C)

{ H

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

(V,C,u) is set

v is set

r is Relation-like Function-like finite set

dom r is finite set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

(V,C,u) is set

V is finite set

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

Fin (PFuncs ({},V)) is non empty cup-closed diff-closed preBoolean set

C is finite Element of Fin (PFuncs ({},V))

({},V,C) is finite set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

(V,C,u) is finite set

PFuncs ((V,C,u),C) is functional non empty set

{ b

( not b

{ b

r is set

v9 is Relation-like Function-like Element of PFuncs ((V,C,u),C)

r is Relation-like Function-like Element of PFuncs ((V,C,u),C)

{ H

{ H

r is set

v9 is Relation-like Function-like Element of PFuncs ((V,C,u),C)

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

(V,C,u) is finite Element of Fin (PFuncs (V,C))

(V,C,u) is finite set

PFuncs ((V,C,u),C) is functional non empty set

{ b

( not b

u ^ (V,C,u) is finite Element of Fin (PFuncs (V,C))

v is set

{ (b

r is Relation-like Function-like Element of PFuncs (V,C)

v9 is Relation-like Function-like Element of PFuncs (V,C)

r \/ v9 is Relation-like set

w is Relation-like Function-like Element of PFuncs ((V,C,u),C)

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

(V,C,u) is finite Element of Fin (PFuncs (V,C))

(V,C,u) is finite set

PFuncs ((V,C,u),C) is functional non empty set

{ b

( not b

v is Relation-like Function-like Element of PFuncs (V,C)

{ b

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

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

(V,C,u) is finite Element of Fin (PFuncs (V,C))

(V,C,u) is finite set

PFuncs ((V,C,u),C) is functional non empty set

{ b

( not b

v is set

r is Relation-like Function-like Element of PFuncs ((V,C,u),C)

[:V,C:] is Relation-like set

bool [:V,C:] is non empty cup-closed diff-closed preBoolean set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

Bottom (SubstLatt (V,C)) is Element of the carrier of (SubstLatt (V,C))

the carrier of (SubstLatt (V,C)) is non empty set

u is functional finite Element of SubstitutionSet (V,C)

(V,C,u) is finite Element of Fin (PFuncs (V,C))

(V,C,u) is finite set

PFuncs ((V,C,u),C) is functional non empty set

{ b

( not b

u ^ (V,C,u) is finite Element of Fin (PFuncs (V,C))

mi (u ^ (V,C,u)) is functional finite Element of SubstitutionSet (V,C)

V is non empty set

C is non empty finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

Top (SubstLatt (V,C)) is Element of the carrier of (SubstLatt (V,C))

the carrier of (SubstLatt (V,C)) is non empty set

u is functional finite Element of SubstitutionSet (V,C)

(V,C,u) is finite Element of Fin (PFuncs (V,C))

(V,C,u) is finite set

PFuncs ((V,C,u),C) is functional non empty set

{ b

( not b

mi (V,C,u) is functional finite Element of SubstitutionSet (V,C)

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

(V,C,u) is finite Element of Fin (PFuncs (V,C))

(V,C,u) is finite set

PFuncs ((V,C,u),C) is functional non empty set

{ b

( not b

v is Relation-like Function-like Element of PFuncs (V,C)

{v} is functional non empty finite set

r is functional finite Element of SubstitutionSet (V,C)

u ^ r is finite Element of Fin (PFuncs (V,C))

dom v is set

w is Relation-like Function-like Element of PFuncs (V,C)

w \/ v is Relation-like set

{ (b

dom w is set

(dom w) /\ (dom v) is set

pf is set

w . pf is set

v . pf is set

sf is Relation-like Function-like set

dom sf is set

rng sf is set

[V] is non empty set

a is Element of [V]

SA is Element of [V]

w . SA is set

v . SA is set

Funcs ((PFuncs (V,C)),[V]) is functional non empty FUNCTION_DOMAIN of PFuncs (V,C),[V]

w is Relation-like PFuncs (V,C) -defined [V] -valued Function-like total quasi_total Element of Funcs ((PFuncs (V,C)),[V])

[u] is non empty set

v9 is non empty finite set

{ H

{ (w . b

pf is finite set

v | pf is Relation-like Function-like finite set

dom (v | pf) is finite set

a is set

SA is Element of [u]

w . SA is set

v is Relation-like Function-like finite set

v9 is Relation-like Function-like Element of PFuncs (V,C)

w . v9 is Element of [V]

dom v9 is set

(dom v9) /\ (dom v) is set

dom v is finite set

rng (v | pf) is finite set

rng v is set

a is Relation-like Function-like set

dom a is set

rng a is set

SA is Relation-like Function-like Element of PFuncs (V,C)

dom SA is set

(dom SA) /\ (dom (v | pf)) is finite set

v is Relation-like Function-like set

w . SA is Element of [V]

v . (w . SA) is set

(v | pf) . (w . SA) is set

(dom SA) /\ (dom v) is set

(dom v) /\ pf is finite set

SA . (w . SA) is set

v . (w . SA) is set

v9 is set

v . v9 is set

(v | pf) . v9 is set

a is Relation-like Function-like Element of PFuncs ((V,C,u),C)

v9 is finite set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

v is finite Element of Fin (PFuncs (V,C))

PFuncs (u,v) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

{ (union { ((b

pf is set

sf is Relation-like Function-like Element of PFuncs (u,v)

{ ((sf . b

union { ((sf . b

dom sf is set

r is functional non empty finite set

{ ((a

union { ((a

{ H

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

v is finite Element of Fin (PFuncs (V,C))

(V,C,u,v) is finite Element of Fin (PFuncs (V,C))

PFuncs (u,v) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

[:u,v:] is Relation-like finite set

bool [:u,v:] is non empty cup-closed diff-closed preBoolean finite V47() set

r is set

v9 is Relation-like Function-like Element of PFuncs (u,v)

{ ((v9 . b

union { ((v9 . b

dom v9 is set

V is set

C is set

u is finite set

PFuncs (C,u) is functional non empty set

Fin (PFuncs (C,u)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (C,u) is non empty Element of bool (Fin (PFuncs (C,u)))

bool (Fin (PFuncs (C,u))) is non empty cup-closed diff-closed preBoolean set

v is finite Element of Fin (PFuncs (C,u))

r is functional finite Element of SubstitutionSet (C,u)

(C,u,v,r) is finite Element of Fin (PFuncs (C,u))

PFuncs (v,r) is functional non empty set

{ (union { ((b

(PFuncs (C,u)) /\ { (union { ((b

v ^ (C,u,v,r) is finite Element of Fin (PFuncs (C,u))

v9 is set

w is set

v9 \/ w is set

[:v,r:] is Relation-like finite set

bool [:v,r:] is non empty cup-closed diff-closed preBoolean finite V47() set

sf is Relation-like v -defined r -valued Function-like finite Element of bool [:v,r:]

{ ((sf . b

union { ((sf . b

dom sf is finite Element of bool v

bool v is non empty cup-closed diff-closed preBoolean finite V47() set

sf . v9 is Relation-like Function-like set

a is Relation-like Function-like Element of PFuncs (C,u)

pf is Relation-like Function-like Element of PFuncs (C,u)

a \ pf is Relation-like Function-like Element of bool a

bool a is non empty cup-closed diff-closed preBoolean set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

u is finite Element of Fin (PFuncs (V,C))

(V,C,u,u) is finite Element of Fin (PFuncs (V,C))

PFuncs (u,u) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

{ ((a

union { ((a

id u is Relation-like u -defined u -valued Function-like one-to-one total quasi_total onto bijective V28() V30() V31() V35() finite Element of bool [:u,u:]

[:u,u:] is Relation-like finite set

bool [:u,u:] is non empty cup-closed diff-closed preBoolean finite V47() set

v is Relation-like Function-like Element of PFuncs (u,u)

dom v is set

{ {} where b

v is Relation-like Function-like Element of PFuncs (u,u)

{ ((v . b

r is set

v9 is Relation-like Function-like Element of PFuncs (V,C)

v . v9 is set

(v . v9) \ v9 is Element of bool (v . v9)

bool (v . v9) is non empty cup-closed diff-closed preBoolean set

v is Relation-like Function-like Element of PFuncs (u,u)

dom v is set

{ ((v . b

union { ((v . b

{ H

{ H

[:V,C:] is Relation-like set

bool [:V,C:] is non empty cup-closed diff-closed preBoolean set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

v is set

r is finite Element of Fin (PFuncs (V,C))

v9 is Relation-like Function-like Element of PFuncs (V,C)

w is Relation-like Function-like Element of PFuncs (V,C)

v9 is set

{ b

( not b

( not b

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

u is Element of the carrier of (SubstLatt (V,C))

v is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

r is functional finite Element of SubstitutionSet (V,C)

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

[:(SubstitutionSet (V,C)),(SubstitutionSet (V,C)):] is Relation-like non empty set

bool [:(SubstitutionSet (V,C)),(SubstitutionSet (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Relation-like SubstitutionSet (V,C) -defined SubstitutionSet (V,C) -valued Function-like non empty total quasi_total Element of bool [:(SubstitutionSet (V,C)),(SubstitutionSet (V,C)):]

v is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

v9 is functional finite Element of SubstitutionSet (V,C)

r is Element of the carrier of (SubstLatt (V,C))

v . r is Element of the carrier of (SubstLatt (V,C))

(V,C,v9) is finite Element of Fin (PFuncs (V,C))

(V,C,v9) is finite set

PFuncs ((V,C,v9),C) is functional non empty set

{ b

( not b

mi (V,C,v9) is functional finite Element of SubstitutionSet (V,C)

u is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

v is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

r is Element of the carrier of (SubstLatt (V,C))

u . r is Element of the carrier of (SubstLatt (V,C))

v9 is functional finite Element of SubstitutionSet (V,C)

(V,C,v9) is finite Element of Fin (PFuncs (V,C))

(V,C,v9) is finite set

PFuncs ((V,C,v9),C) is functional non empty set

{ b

( not b

mi (V,C,v9) is functional finite Element of SubstitutionSet (V,C)

v . r is Element of the carrier of (SubstLatt (V,C))

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

v is Element of the carrier of (SubstLatt (V,C))

r is Element of the carrier of (SubstLatt (V,C))

v9 is functional finite Element of SubstitutionSet (V,C)

w is functional finite Element of SubstitutionSet (V,C)

(V,C,v9,w) is finite Element of Fin (PFuncs (V,C))

PFuncs (v9,w) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

mi (V,C,v9,w) is functional finite Element of SubstitutionSet (V,C)

pf is Element of the carrier of (SubstLatt (V,C))

sf is functional finite Element of SubstitutionSet (V,C)

a is functional finite Element of SubstitutionSet (V,C)

(V,C,sf,a) is finite Element of Fin (PFuncs (V,C))

PFuncs (sf,a) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

mi (V,C,sf,a) is functional finite Element of SubstitutionSet (V,C)

v is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

r is Element of the carrier of (SubstLatt (V,C))

v9 is Element of the carrier of (SubstLatt (V,C))

v . (r,v9) is Element of the carrier of (SubstLatt (V,C))

w is functional finite Element of SubstitutionSet (V,C)

pf is functional finite Element of SubstitutionSet (V,C)

(V,C,w,pf) is finite Element of Fin (PFuncs (V,C))

PFuncs (w,pf) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

mi (V,C,w,pf) is functional finite Element of SubstitutionSet (V,C)

u is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

v is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

r is Element of the carrier of (SubstLatt (V,C))

v9 is Element of the carrier of (SubstLatt (V,C))

u . (r,v9) is Element of the carrier of (SubstLatt (V,C))

w is functional finite Element of SubstitutionSet (V,C)

pf is functional finite Element of SubstitutionSet (V,C)

(V,C,w,pf) is finite Element of Fin (PFuncs (V,C))

PFuncs (w,pf) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

mi (V,C,w,pf) is functional finite Element of SubstitutionSet (V,C)

v . (r,v9) is Element of the carrier of (SubstLatt (V,C))

u is Element of the carrier of (SubstLatt (V,C))

bool u is non empty cup-closed diff-closed preBoolean set

Fin the carrier of (SubstLatt (V,C)) is non empty cup-closed diff-closed preBoolean set

r is set

v is functional finite Element of SubstitutionSet (V,C)

v is Relation-like Function-like set

dom v is set

r is set

v . r is set

u \ r is Element of bool u

[: the carrier of (SubstLatt (V,C)),(Fin (PFuncs (V,C))):] is Relation-like non empty set

bool [: the carrier of (SubstLatt (V,C)),(Fin (PFuncs (V,C))):] is non empty cup-closed diff-closed preBoolean set

v9 is Element of the carrier of (SubstLatt (V,C))

u \ v9 is Element of bool u

r is Relation-like the carrier of (SubstLatt (V,C)) -defined Fin (PFuncs (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)),(Fin (PFuncs (V,C))):]

r . v9 is finite Element of Fin (PFuncs (V,C))

v9 is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

w is Element of the carrier of (SubstLatt (V,C))

v9 . w is Element of the carrier of (SubstLatt (V,C))

u \ w is Element of bool u

v is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

r is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

v9 is Element of the carrier of (SubstLatt (V,C))

v . v9 is Element of the carrier of (SubstLatt (V,C))

u \ v9 is Element of bool u

r . v9 is Element of the carrier of (SubstLatt (V,C))

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

u is Element of the carrier of (SubstLatt (V,C))

v is Element of the carrier of (SubstLatt (V,C))

(V,C,v) is finite Element of Fin the carrier of (SubstLatt (V,C))

Fin the carrier of (SubstLatt (V,C)) is non empty cup-closed diff-closed preBoolean set

bool v is non empty cup-closed diff-closed preBoolean set

(V,C,v) is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

(V,C,v) . u is Element of the carrier of (SubstLatt (V,C))

u "\/" ((V,C,v) . u) is Element of the carrier of (SubstLatt (V,C))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

v \ u is Element of bool v

the L_join of (SubstLatt (V,C)) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

the L_join of (SubstLatt (V,C)) . (u,((V,C,v) . u)) is Element of the carrier of (SubstLatt (V,C))

v9 is functional finite Element of SubstitutionSet (V,C)

w is functional finite Element of SubstitutionSet (V,C)

v9 \/ w is finite Element of Fin (PFuncs (V,C))

mi (v9 \/ w) is functional finite Element of SubstitutionSet (V,C)

r is functional finite Element of SubstitutionSet (V,C)

mi r is functional finite Element of SubstitutionSet (V,C)

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is Element of the carrier of (SubstLatt (V,C))

(V,C,u) is finite Element of Fin the carrier of (SubstLatt (V,C))

Fin the carrier of (SubstLatt (V,C)) is non empty cup-closed diff-closed preBoolean set

bool u is non empty cup-closed diff-closed preBoolean set

(V,C,u) is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

v is Relation-like Function-like Element of PFuncs (V,C)

{v} is functional non empty finite set

r is finite Element of Fin (PFuncs (V,C))

{ H

w is Element of the carrier of (SubstLatt (V,C))

pf is functional finite Element of SubstitutionSet (V,C)

pf ^ r is finite Element of Fin (PFuncs (V,C))

(V,C,u) . pf is set

sf is Relation-like Function-like Element of PFuncs (V,C)

a is Relation-like Function-like Element of PFuncs (V,C)

v is Relation-like Function-like Element of PFuncs (V,C)

SA is Relation-like Function-like Element of PFuncs (V,C)

{ H

{ H

sf is Relation-like Function-like Element of PFuncs (V,C)

a is Relation-like Function-like Element of PFuncs (V,C)

sf is Relation-like Function-like Element of PFuncs (V,C)

a is Relation-like Function-like Element of PFuncs (V,C)

{ H

{ H

{ H

{ H

{ (b

sf is set

a is Relation-like Function-like Element of PFuncs (V,C)

a \/ v is Relation-like set

sf is Relation-like Function-like Element of PFuncs (V,C)

u \ pf is Element of bool u

V is set

C is finite set

PFuncs (V,C) is functional non empty set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

[:(PFuncs (V,C)),(SubstitutionSet (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)),(SubstitutionSet (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Relation-like PFuncs (V,C) -defined SubstitutionSet (V,C) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)),(SubstitutionSet (V,C)):]

v is set

r is Relation-like Function-like Element of PFuncs (V,C)

u . r is functional finite Element of SubstitutionSet (V,C)

{.r.} is functional non empty finite Element of Fin (PFuncs (V,C))

mi {.r.} is functional finite Element of SubstitutionSet (V,C)

u . v is set

dom u is functional non empty Element of bool (PFuncs (V,C))

bool (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

v is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

r is Relation-like Function-like Element of PFuncs (V,C)

v . r is Element of the carrier of (SubstLatt (V,C))

{.r.} is functional non empty finite Element of Fin (PFuncs (V,C))

mi {.r.} is functional finite Element of SubstitutionSet (V,C)

u is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

v is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

r is Relation-like Function-like Element of PFuncs (V,C)

u . r is Element of the carrier of (SubstLatt (V,C))

{.r.} is functional non empty finite Element of Fin (PFuncs (V,C))

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

mi {.r.} is functional finite Element of SubstitutionSet (V,C)

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

v . r is Element of the carrier of (SubstLatt (V,C))

V is set

C is finite set

PFuncs (V,C) is functional non empty set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

(V,C) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Relation-like Function-like Element of PFuncs (V,C)

(V,C) . u is Element of the carrier of (SubstLatt (V,C))

{u} is functional non empty finite set

v is Relation-like Function-like Element of PFuncs (V,C)

r is Relation-like Function-like Element of PFuncs (V,C)

v is set

{.u.} is functional non empty finite Element of Fin (PFuncs (V,C))

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

( not b

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

mi {.u.} is functional finite Element of SubstitutionSet (V,C)

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

(V,C) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

the carrier of (SubstLatt (V,C)) is non empty set

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

singleton (PFuncs (V,C)) is Relation-like PFuncs (V,C) -defined Fin (PFuncs (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)),(Fin (PFuncs (V,C))):]

[:(PFuncs (V,C)),(Fin (PFuncs (V,C))):] is Relation-like non empty set

bool [:(PFuncs (V,C)),(Fin (PFuncs (V,C))):] is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

FinJoin (u,(V,C)) is Element of the carrier of (SubstLatt (V,C))

FinUnion (u,(singleton (PFuncs (V,C)))) is finite Element of Fin (PFuncs (V,C))

mi (FinUnion (u,(singleton (PFuncs (V,C))))) is functional finite Element of SubstitutionSet (V,C)

v is set

r is Relation-like Function-like Element of PFuncs (V,C)

(singleton (PFuncs (V,C))) . r is finite Element of Fin (PFuncs (V,C))

{ b

( not b

( not b

v9 is finite set

w is Relation-like Function-like Element of PFuncs (V,C)

(singleton (PFuncs (V,C))) . w is finite Element of Fin (PFuncs (V,C))

pf is finite Element of Fin (PFuncs (V,C))

[:(Fin (PFuncs (V,C))),(SubstitutionSet (V,C)):] is Relation-like non empty set

bool [:(Fin (PFuncs (V,C))),(SubstitutionSet (V,C)):] is non empty cup-closed diff-closed preBoolean set

v is Relation-like Fin (PFuncs (V,C)) -defined SubstitutionSet (V,C) -valued Function-like non empty total quasi_total Element of bool [:(Fin (PFuncs (V,C))),(SubstitutionSet (V,C)):]

[:(Fin (PFuncs (V,C))), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(Fin (PFuncs (V,C))), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

r is Relation-like Fin (PFuncs (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(Fin (PFuncs (V,C))), the carrier of (SubstLatt (V,C)):]

v9 is finite Element of Fin (PFuncs (V,C))

r . v9 is Element of the carrier of (SubstLatt (V,C))

mi v9 is functional finite Element of SubstitutionSet (V,C)

w is finite Element of Fin (PFuncs (V,C))

r . w is Element of the carrier of (SubstLatt (V,C))

mi w is functional finite Element of SubstitutionSet (V,C)

v9 \/ w is finite Element of Fin (PFuncs (V,C))

r . (v9 \/ w) is Element of the carrier of (SubstLatt (V,C))

mi (v9 \/ w) is functional finite Element of SubstitutionSet (V,C)

(mi v9) \/ w is finite Element of Fin (PFuncs (V,C))

mi ((mi v9) \/ w) is functional finite Element of SubstitutionSet (V,C)

(mi v9) \/ (mi w) is finite Element of Fin (PFuncs (V,C))

mi ((mi v9) \/ (mi w)) is functional finite Element of SubstitutionSet (V,C)

the L_join of (SubstLatt (V,C)) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

the L_join of (SubstLatt (V,C)) . ((r . v9),(r . w)) is Element of the carrier of (SubstLatt (V,C))

v9 is set

w is Relation-like Function-like Element of PFuncs (V,C)

{w} is functional non empty finite set

r * (singleton (PFuncs (V,C))) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

(r * (singleton (PFuncs (V,C)))) | u is Relation-like PFuncs (V,C) -defined u -defined PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like finite Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

((r * (singleton (PFuncs (V,C)))) | u) . v9 is set

(r * (singleton (PFuncs (V,C)))) . v9 is set

(singleton (PFuncs (V,C))) . w is finite Element of Fin (PFuncs (V,C))

r . ((singleton (PFuncs (V,C))) . w) is Element of the carrier of (SubstLatt (V,C))

{v9} is non empty finite set

r . {v9} is set

pf is functional finite Element of SubstitutionSet (V,C)

mi pf is functional finite Element of SubstitutionSet (V,C)

(V,C) . w is Element of the carrier of (SubstLatt (V,C))

(V,C) | u is Relation-like PFuncs (V,C) -defined u -defined PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like finite Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

((V,C) | u) . v9 is set

rng (singleton (PFuncs (V,C))) is non empty Element of bool (Fin (PFuncs (V,C)))

dom (V,C) is functional non empty Element of bool (PFuncs (V,C))

bool (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

dom ((V,C) | u) is functional finite Element of bool u

bool u is non empty cup-closed diff-closed preBoolean finite V47() set

{}. (PFuncs (V,C)) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V47() Element of Fin (PFuncs (V,C))

r . ({}. (PFuncs (V,C))) is Element of the carrier of (SubstLatt (V,C))

mi ({}. (PFuncs (V,C))) is functional finite Element of SubstitutionSet (V,C)

Bottom (SubstLatt (V,C)) is Element of the carrier of (SubstLatt (V,C))

the_unity_wrt the L_join of (SubstLatt (V,C)) is Element of the carrier of (SubstLatt (V,C))

dom r is non empty Element of bool (Fin (PFuncs (V,C)))

dom (r * (singleton (PFuncs (V,C)))) is functional non empty Element of bool (PFuncs (V,C))

dom (singleton (PFuncs (V,C))) is functional non empty Element of bool (PFuncs (V,C))

dom ((r * (singleton (PFuncs (V,C)))) | u) is functional finite Element of bool u

v9 is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

FinJoin (u,v9) is Element of the carrier of (SubstLatt (V,C))

the L_join of (SubstLatt (V,C)) $$ (u,v9) is Element of the carrier of (SubstLatt (V,C))

r . (FinUnion (u,(singleton (PFuncs (V,C))))) is Element of the carrier of (SubstLatt (V,C))

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

(V,C) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

the carrier of (SubstLatt (V,C)) is non empty set

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is functional finite Element of SubstitutionSet (V,C)

FinJoin (u,(V,C)) is Element of the carrier of (SubstLatt (V,C))

singleton (PFuncs (V,C)) is Relation-like PFuncs (V,C) -defined Fin (PFuncs (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)),(Fin (PFuncs (V,C))):]

[:(PFuncs (V,C)),(Fin (PFuncs (V,C))):] is Relation-like non empty set

bool [:(PFuncs (V,C)),(Fin (PFuncs (V,C))):] is non empty cup-closed diff-closed preBoolean set

FinUnion (u,(singleton (PFuncs (V,C)))) is finite Element of Fin (PFuncs (V,C))

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

u is Element of the carrier of (SubstLatt (V,C))

v is Element of the carrier of (SubstLatt (V,C))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u "/\" v is Element of the carrier of (SubstLatt (V,C))

the L_meet of (SubstLatt (V,C)) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

r is functional finite Element of SubstitutionSet (V,C)

v9 is functional finite Element of SubstitutionSet (V,C)

the L_meet of (SubstLatt (V,C)) . (r,v9) is set

r ^ v9 is finite Element of Fin (PFuncs (V,C))

mi (r ^ v9) is functional finite Element of SubstitutionSet (V,C)

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

u is Element of the carrier of (SubstLatt (V,C))

(V,C,u) is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

v is Element of the carrier of (SubstLatt (V,C))

(V,C,u) . v is Element of the carrier of (SubstLatt (V,C))

u \ v is Element of bool u

bool u is non empty cup-closed diff-closed preBoolean set

r is set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

(V,C) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Relation-like Function-like Element of PFuncs (V,C)

(V,C) . u is Element of the carrier of (SubstLatt (V,C))

{u} is functional non empty finite set

v is set

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

(V,C) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

(V,C) is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Element of the carrier of (SubstLatt (V,C))

(V,C) . u is Element of the carrier of (SubstLatt (V,C))

v is functional finite Element of SubstitutionSet (V,C)

r is functional finite Element of SubstitutionSet (V,C)

r ^ v is finite Element of Fin (PFuncs (V,C))

v9 is Relation-like Function-like Element of PFuncs (V,C)

{v9} is functional non empty finite set

(V,C) . v9 is Element of the carrier of (SubstLatt (V,C))

w is set

(V,C,r) is finite Element of Fin (PFuncs (V,C))

(V,C,r) is finite set

PFuncs ((V,C,r),C) is functional non empty set

{ b

( not b

pf is Relation-like Function-like Element of PFuncs (V,C)

sf is finite set

mi (V,C,r) is functional finite Element of SubstitutionSet (V,C)

a is set

SA is set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

(V,C) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Relation-like Function-like finite Element of PFuncs (V,C)

(V,C) . u is Element of the carrier of (SubstLatt (V,C))

{u} is functional non empty finite V47() set

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

u is Element of the carrier of (SubstLatt (V,C))

v is Element of the carrier of (SubstLatt (V,C))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u "/\" v is Element of the carrier of (SubstLatt (V,C))

the L_meet of (SubstLatt (V,C)) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

the L_meet of (SubstLatt (V,C)) . (u,v) is Element of the carrier of (SubstLatt (V,C))

r is functional finite Element of SubstitutionSet (V,C)

v9 is functional finite Element of SubstitutionSet (V,C)

r ^ v9 is finite Element of Fin (PFuncs (V,C))

mi (r ^ v9) is functional finite Element of SubstitutionSet (V,C)

w is set

V is set

C is finite set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

u is Relation-like Function-like Element of PFuncs (V,C)

v is functional finite Element of SubstitutionSet (V,C)

r is functional finite Element of SubstitutionSet (V,C)

(V,C,v,r) is finite Element of Fin (PFuncs (V,C))

PFuncs (v,r) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

w is Relation-like Function-like Element of PFuncs (V,C)

w \/ u is Relation-like set

pf is set

sf is Relation-like Function-like Element of PFuncs (V,C)

a is Relation-like Function-like Element of PFuncs (V,C)

Funcs ((PFuncs (V,C)),(PFuncs (V,C))) is functional non empty FUNCTION_DOMAIN of PFuncs (V,C), PFuncs (V,C)

w is Relation-like PFuncs (V,C) -defined PFuncs (V,C) -valued Function-like total quasi_total Element of Funcs ((PFuncs (V,C)),(PFuncs (V,C)))

w | v is Relation-like PFuncs (V,C) -defined v -defined PFuncs (V,C) -defined PFuncs (V,C) -valued Function-like finite Element of bool [:(PFuncs (V,C)),(PFuncs (V,C)):]

[:(PFuncs (V,C)),(PFuncs (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)),(PFuncs (V,C)):] is non empty cup-closed diff-closed preBoolean set

sf is Relation-like Function-like set

dom sf is set

rng sf is set

[:v,(PFuncs (V,C)):] is Relation-like set

bool [:v,(PFuncs (V,C)):] is non empty cup-closed diff-closed preBoolean set

dom (w | v) is functional finite Element of bool v

bool v is non empty cup-closed diff-closed preBoolean finite V47() set

a is set

(w | v) . a is Relation-like Function-like set

SA is Relation-like Function-like Element of PFuncs (V,C)

(w | v) . SA is Relation-like Function-like set

sf . SA is set

[:v,r:] is Relation-like finite set

bool [:v,r:] is non empty cup-closed diff-closed preBoolean finite V47() set

rng (w | v) is functional finite Element of bool (PFuncs (V,C))

bool (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

v9 is Element of the carrier of (SubstLatt (V,C))

a is set

(w | v) . a is Relation-like Function-like set

a \/ u is set

SA is Relation-like Function-like Element of PFuncs (V,C)

(w | v) . SA is Relation-like Function-like set

sf . SA is set

a is Relation-like Function-like Element of PFuncs (v,r)

{ ((a . b

union { ((a . b

v is set

v9 is set

dv is Relation-like Function-like Element of PFuncs (V,C)

a . dv is set

(a . dv) \ dv is Element of bool (a . dv)

bool (a . dv) is non empty cup-closed diff-closed preBoolean set

dv \/ u is Relation-like set

v is Relation-like Function-like Element of PFuncs (V,C)

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

PFuncs (V,C) is functional non empty set

(V,C) is Relation-like PFuncs (V,C) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):]

[:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:(PFuncs (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

(V,C) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Element of the carrier of (SubstLatt (V,C))

v is Element of the carrier of (SubstLatt (V,C))

(V,C) . (u,v) is Element of the carrier of (SubstLatt (V,C))

r is Relation-like Function-like finite Element of PFuncs (V,C)

(V,C) . r is Element of the carrier of (SubstLatt (V,C))

u "/\" ((V,C) . r) is Element of the carrier of (SubstLatt (V,C))

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

pf is functional finite Element of SubstitutionSet (V,C)

sf is set

v9 is functional finite Element of SubstitutionSet (V,C)

a is Relation-like Function-like Element of PFuncs (V,C)

sf \/ r is set

{ (b

v9 ^ pf is finite Element of Fin (PFuncs (V,C))

mi (v9 ^ pf) is functional finite Element of SubstitutionSet (V,C)

SA is set

the L_meet of (SubstLatt (V,C)) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

the L_meet of (SubstLatt (V,C)) . (u,((V,C) . r)) is Element of the carrier of (SubstLatt (V,C))

v is set

v9 is set

sf is set

w is functional finite Element of SubstitutionSet (V,C)

(V,C,v9,w) is finite Element of Fin (PFuncs (V,C))

PFuncs (v9,w) is functional non empty set

{ (union { ((b

(PFuncs (V,C)) /\ { (union { ((b

a is set

mi (V,C,v9,w) is functional finite Element of SubstitutionSet (V,C)

SA is set

v is set

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

(V,C) is Relation-like the carrier of (SubstLatt (V,C)) -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

Bottom (SubstLatt (V,C)) is Element of the carrier of (SubstLatt (V,C))

u is Element of the carrier of (SubstLatt (V,C))

(V,C) . u is Element of the carrier of (SubstLatt (V,C))

u "/\" ((V,C) . u) is Element of the carrier of (SubstLatt (V,C))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

the L_meet of (SubstLatt (V,C)) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

H

v is functional finite Element of SubstitutionSet (V,C)

(V,C,v) is finite Element of Fin (PFuncs (V,C))

(V,C,v) is finite set

PFuncs ((V,C,v),C) is functional non empty set

{ b

( not b

mi (V,C,v) is functional finite Element of SubstitutionSet (V,C)

H

v ^ (mi (V,C,v)) is finite Element of Fin (PFuncs (V,C))

mi (v ^ (mi (V,C,v))) is functional finite Element of SubstitutionSet (V,C)

v ^ (V,C,v) is finite Element of Fin (PFuncs (V,C))

mi (v ^ (V,C,v)) is functional finite Element of SubstitutionSet (V,C)

V is set

C is finite set

SubstLatt (V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() LattStr

the carrier of (SubstLatt (V,C)) is non empty set

(V,C) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):]

[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

[:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is Relation-like non empty set

bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C)):] is non empty cup-closed diff-closed preBoolean set

u is Element of the carrier of (SubstLatt (V,C))

v is Element of the carrier of (SubstLatt (V,C))

(V,C) . (u,v) is Element of the carrier of (SubstLatt (V,C))

u "/\" ((V,C) . (u,v)) is Element of the carrier of (SubstLatt (V,C))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

SubstitutionSet (V,C) is non empty Element of bool (Fin (PFuncs (V,C)))

bool (Fin (PFuncs (V,C))) is non empty cup-closed diff-closed preBoolean set

w is set

the L_meet of (SubstLatt (V,C)) is Relation-like [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] -defined the carrier of (SubstLatt (V,C)) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):], the carrier of (SubstLatt (V,C))