:: 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } 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))
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₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : S₁[b₁] } is set
r is set
v9 is Relation-like Function-like Element of PFuncs (V,C)
dom v9 is set
{ H₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
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₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : S₁[b₁] } is set
r is Relation-like Function-like Element of PFuncs (V,C)
{ H₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : S₂[b₁] } 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
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in u or not b₁ tolerates b₂ ) } is set
{ b₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : verum } is set
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₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : S₂[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : S₁[b₁] } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in u or not b₁ tolerates b₂ ) } is set
u ^ (V,C,u) is finite Element of Fin (PFuncs (V,C))
v is set
{ (b₁ \/ b₂) where b₁, b₂ is Relation-like Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in (V,C,u) & b₁ tolerates b₂ ) } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in u or not b₁ tolerates b₂ ) } is set
v is Relation-like Function-like Element of PFuncs (V,C)
{ b₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : S₁[b₁] } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in u or not b₁ tolerates b₂ ) } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in u or not b₁ tolerates b₂ ) } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in u or not b₁ tolerates b₂ ) } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in u or not b₁ tolerates b₂ ) } is set
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₁ \/ b₂) where b₁, b₂ is Relation-like Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in r & b₁ tolerates b₂ ) } is set
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₁(b₁) where b₁ is Element of v9 : S₂[b₁] } is set
{ (w . b₁) where b₁ is Element of [u] : verum } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in u } ) where b₁ is Relation-like Function-like Element of PFuncs (u,v) : dom b₁ = u } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in u } ) where b₁ is Relation-like Function-like Element of PFuncs (u,v) : dom b₁ = u } is set
{ (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in u } ) where b₁ is Relation-like Function-like Element of PFuncs (u,v) : ( b₁ in PFuncs (u,v) & dom b₁ = u ) } is set
pf is set
sf is Relation-like Function-like Element of PFuncs (u,v)
{ ((sf . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
union { ((sf . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
dom sf is set
r is functional non empty finite set
{ ((a₁ . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
union { ((a₁ . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
{ H₁(b₁) where b₁ is Relation-like Function-like Element of r : S₁[b₁] } 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 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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in u } ) where b₁ is Relation-like Function-like Element of PFuncs (u,v) : dom b₁ = u } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in u } ) where b₁ is Relation-like Function-like Element of PFuncs (u,v) : dom b₁ = u } is set
[: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₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
union { ((v9 . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (C,u) : b₂ in v } ) where b₁ is Relation-like Function-like Element of PFuncs (v,r) : dom b₁ = v } is set
(PFuncs (C,u)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (C,u) : b₂ in v } ) where b₁ is Relation-like Function-like Element of PFuncs (v,r) : dom b₁ = v } is set
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₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (C,u) : b₁ in v } is set
union { ((sf . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (C,u) : b₁ in v } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in u } ) where b₁ is Relation-like Function-like Element of PFuncs (u,u) : dom b₁ = u } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in u } ) where b₁ is Relation-like Function-like Element of PFuncs (u,u) : dom b₁ = u } is set
{ ((a₁ . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
union { ((a₁ . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
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₁ is Relation-like Function-like Element of PFuncs (u,u) : S₁[b₁] } is set
v is Relation-like Function-like Element of PFuncs (u,u)
{ ((v . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
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₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
union { ((v . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in u } is set
{ H₂(b₁) where b₁ is Relation-like Function-like Element of PFuncs (u,u) : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs (u,u) : S₁[b₁] } is set
[: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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } 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
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,v9),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in v9 or not b₁ tolerates b₂ ) } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,v9),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in v9 or not b₁ tolerates b₂ ) } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in v9 } ) where b₁ is Relation-like Function-like Element of PFuncs (v9,w) : dom b₁ = v9 } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in v9 } ) where b₁ is Relation-like Function-like Element of PFuncs (v9,w) : dom b₁ = v9 } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in sf } ) where b₁ is Relation-like Function-like Element of PFuncs (sf,a) : dom b₁ = sf } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in sf } ) where b₁ is Relation-like Function-like Element of PFuncs (sf,a) : dom b₁ = sf } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in w } ) where b₁ is Relation-like Function-like Element of PFuncs (w,pf) : dom b₁ = w } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in w } ) where b₁ is Relation-like Function-like Element of PFuncs (w,pf) : dom b₁ = w } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in w } ) where b₁ is Relation-like Function-like Element of PFuncs (w,pf) : dom b₁ = w } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in w } ) where b₁ is Relation-like Function-like Element of PFuncs (w,pf) : dom b₁ = w } is set
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₁(b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : ( H₁(b₁) in u & S₂[b₁] ) } is set
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₃(b₁,b₂) where b₁, b₂ is Relation-like Function-like Element of PFuncs (V,C) : S₃[b₁,b₂] } is set
{ H₃(b₁,b₂) where b₁, b₂ is Relation-like Function-like Element of PFuncs (V,C) : S₄[b₁,b₂] } is set
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₄(b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : S₅[b₁] } is set
{ H₄(b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : S₁[b₁] } is set
{ H₂(b₁,b₂) where b₁, b₂ is Relation-like Function-like Element of PFuncs (V,C) : ( b₂ = v & S₆[b₁,b₂] ) } is set
{ H₂(b₁,v) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : S₆[b₁,v] } is set
{ (b₁ \/ v) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : ( not b₁ tolerates v & b₁ in u & b₁ tolerates v ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is 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
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,r),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in r or not b₁ tolerates b₂ ) } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in v } ) where b₁ is Relation-like Function-like Element of PFuncs (v,r) : dom b₁ = v } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in v } ) where b₁ is Relation-like Function-like Element of PFuncs (v,r) : dom b₁ = v } is 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
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₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in v9 } is set
union { ((a . b₁) \ b₁) where b₁ is Relation-like Function-like Element of PFuncs (V,C) : b₁ in v9 } is set
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₁ \/ b₂) where b₁, b₂ is Relation-like Function-like Element of PFuncs (V,C) : ( b₁ in v9 & b₂ in pf & b₁ tolerates b₂ ) } is set
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₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in v9 } ) where b₁ is Relation-like Function-like Element of PFuncs (v9,w) : dom b₁ = v9 } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in v9 } ) where b₁ is Relation-like Function-like Element of PFuncs (v9,w) : dom b₁ = v9 } is set
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,C) . (u,((V,C) . u)) is Element of the carrier of (SubstLatt (V,C))
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₁ where b₁ is Relation-like Function-like Element of PFuncs ((V,C,v),C) : for b₂ being Relation-like Function-like Element of PFuncs (V,C) holds
( not b₂ in v or not b₁ tolerates b₂ ) } is set
mi (V,C,v) is functional finite Element of SubstitutionSet (V,C)
H₁(V,C) . (u,(mi (V,C,v))) is set
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)):]
H₁(V,C) . (u,((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)
(V,C,r,v9) is finite Element of Fin (PFuncs (V,C))
PFuncs (r,v9) is functional non empty set
{ (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in r } ) where b₁ is Relation-like Function-like Element of PFuncs (r,v9) : dom b₁ = r } is set
(PFuncs (V,C)) /\ { (union { ((b₁ . b₂) \ b₂) where b₂ is Relation-like Function-like Element of PFuncs (V,C) : b₂ in r } ) where b₁ is Relation-like Function-like Element of PFuncs (r,v9) : dom b₁ = r } is set
mi (V,C,r,v9) is functional finite Element of SubstitutionSet (V,C)
H₁(V,C) . (u,(mi (V,C,r,v9))) is set
r ^ (mi (V,C,r,v9)) is finite Element of Fin (PFuncs (V,C))
mi (r ^ (mi (V,C,r,v9))) is functional finite Element of SubstitutionSet (V,C)
r ^ (V,C,r,v9) is finite Element of Fin (PFuncs (V,C))
mi (r ^ (V,C,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
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
(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)):]
bool [: the carrier of (SubstLatt (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)):]
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)):]
v is Element of the carrier of (SubstLatt (V,C))
(V,C) [:] ((V,C,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)):]
H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,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)):]
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 Element of the carrier of (SubstLatt (V,C))
(V,C,u) . w is Element of the carrier of (SubstLatt (V,C))
(V,C) . w is Element of the carrier of (SubstLatt (V,C))
(V,C) . (((V,C,u) . w),v) is Element of the carrier of (SubstLatt (V,C))
((V,C) . w) "/\" ((V,C) . (((V,C,u) . w),v)) is Element of the carrier of (SubstLatt (V,C))
w "/\" (((V,C) . w) "/\" ((V,C) . (((V,C,u) . w),v))) is Element of the carrier of (SubstLatt (V,C))
w "/\" ((V,C) . w) is Element of the carrier of (SubstLatt (V,C))
(w "/\" ((V,C) . w)) "/\" ((V,C) . (((V,C,u) . w),v)) is Element of the carrier of (SubstLatt (V,C))
Bottom (SubstLatt (V,C)) is Element of the carrier of (SubstLatt (V,C))
(Bottom (SubstLatt (V,C))) "/\" ((V,C) . (((V,C,u) . w),v)) 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
w "\/" ((V,C,u) . w) is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) [;] (u,(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,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)):]
(H₁(V,C) [;] (u,(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v)))))) . w is Element of the carrier of (SubstLatt (V,C))
(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v)))) . w is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) . (u,((H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v)))) . w)) is Element of the carrier of (SubstLatt (V,C))
u "/\" ((H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v)))) . w) is Element of the carrier of (SubstLatt (V,C))
((V,C) [:] ((V,C,u),v)) . w is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) . (((V,C) . w),(((V,C) [:] ((V,C,u),v)) . w)) is Element of the carrier of (SubstLatt (V,C))
u "/\" (H₁(V,C) . (((V,C) . w),(((V,C) [:] ((V,C,u),v)) . w))) is Element of the carrier of (SubstLatt (V,C))
((V,C) . w) "/\" (((V,C) [:] ((V,C,u),v)) . w) is Element of the carrier of (SubstLatt (V,C))
u "/\" (((V,C) . w) "/\" (((V,C) [:] ((V,C,u),v)) . w)) is Element of the carrier of (SubstLatt (V,C))
u "/\" (((V,C) . w) "/\" ((V,C) . (((V,C,u) . w),v))) is Element of the carrier of (SubstLatt (V,C))
((V,C,u) . w) "/\" (((V,C) . w) "/\" ((V,C) . (((V,C,u) . w),v))) is Element of the carrier of (SubstLatt (V,C))
(w "/\" (((V,C) . w) "/\" ((V,C) . (((V,C,u) . w),v)))) "\/" (((V,C,u) . w) "/\" (((V,C) . w) "/\" ((V,C) . (((V,C,u) . w),v)))) is Element of the carrier of (SubstLatt (V,C))
((V,C) . (((V,C,u) . w),v)) "/\" ((V,C) . w) is Element of the carrier of (SubstLatt (V,C))
((V,C,u) . w) "/\" (((V,C) . (((V,C,u) . w),v)) "/\" ((V,C) . w)) is Element of the carrier of (SubstLatt (V,C))
((V,C,u) . w) "/\" ((V,C) . (((V,C,u) . w),v)) is Element of the carrier of (SubstLatt (V,C))
(((V,C,u) . w) "/\" ((V,C) . (((V,C,u) . w),v))) "/\" ((V,C) . w) is Element of the carrier of (SubstLatt (V,C))
FinJoin ((V,C,u),(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v))))) is Element of the carrier of (SubstLatt (V,C))
u "/\" H₂(u,v) is Element of the carrier of (SubstLatt (V,C))
FinJoin ((V,C,u),(H₁(V,C) [;] (u,(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v))))))) is Element of the carrier of (SubstLatt (V,C))
u "/\" v is Element of the carrier of (SubstLatt (V,C))
w is Element of the carrier of (SubstLatt (V,C))
v9 is functional finite Element of SubstitutionSet (V,C)
(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
FinJoin (v9,(V,C)) is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) [;] (u,(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)):]
FinJoin (v9,(H₁(V,C) [;] (u,(V,C)))) is Element of the carrier of (SubstLatt (V,C))
(V,C) [:] ((V,C,u),w) 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)):]
a is Relation-like Function-like Element of PFuncs (V,C)
{.a.} is functional non empty finite Element of Fin (PFuncs (V,C))
SA is finite Element of Fin (PFuncs (V,C))
v is functional finite Element of SubstitutionSet (V,C)
v ^ SA is finite Element of Fin (PFuncs (V,C))
(V,C,u) . v is set
v9 is Element of the carrier of (SubstLatt (V,C))
(V,C,u) . v9 is Element of the carrier of (SubstLatt (V,C))
(H₁(V,C) [;] (u,(V,C))) . a is Element of the carrier of (SubstLatt (V,C))
(V,C) . a is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) . (u,((V,C) . a)) is Element of the carrier of (SubstLatt (V,C))
u "/\" ((V,C) . a) is Element of the carrier of (SubstLatt (V,C))
{a} is functional non empty finite set
SS is functional finite Element of SubstitutionSet (V,C)
v ^ SS is finite Element of Fin (PFuncs (V,C))
(V,C) . v9 is Element of the carrier of (SubstLatt (V,C))
((V,C,u) . v9) "/\" ((V,C) . a) is Element of the carrier of (SubstLatt (V,C))
(V,C) . (((V,C,u) . v9),w) is Element of the carrier of (SubstLatt (V,C))
((V,C) [:] ((V,C,u),w)) . v9 is Element of the carrier of (SubstLatt (V,C))
((V,C) . v9) "/\" (((V,C) [:] ((V,C,u),w)) . v9) is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) . (((V,C) . v9),(((V,C) [:] ((V,C,u),w)) . v9)) is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),w))) 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)):]
(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),w)))) . v9 is Element of the carrier of (SubstLatt (V,C))
FinJoin ((V,C,u),(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),w))))) 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,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
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
(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)):]
bool [: the carrier of (SubstLatt (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)):]
(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,C) [:] ((V,C,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)):]
H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,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)):]
FinJoin ((V,C,u),(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v))))) is Element of 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))
u "/\" r is Element of the carrier of (SubstLatt (V,C))
v9 is Element of the carrier of (SubstLatt (V,C))
u "/\" 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
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() implicative Heyting LattStr
the carrier of (SubstLatt (V,C)) is non empty 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)):] 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
(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)):]
bool [: the carrier of (SubstLatt (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)):]
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)):]
v is Element of the carrier of (SubstLatt (V,C))
u => v is Element of the carrier of (SubstLatt (V,C))
(V,C) [:] ((V,C,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)):]
the L_meet of (SubstLatt (V,C)) .: ((V,C),((V,C) [:] ((V,C,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)):]
FinJoin ((V,C,u),( the L_meet of (SubstLatt (V,C)) .: ((V,C),((V,C) [:] ((V,C,u),v))))) is Element of the carrier of (SubstLatt (V,C))
H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,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)):]
FinJoin ((V,C,u),(H₁(V,C) .: ((V,C),((V,C) [:] ((V,C,u),v))))) is Element of 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))
u "/\" H₂(u,v) is Element of the carrier of (SubstLatt (V,C))