:: HEYTING2 semantic presentation

K129() is set

1 is non empty 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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 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))
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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

dom v9 is finite 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

dom r is finite 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
{ H1(b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : S1[b1] } is set
r is set
v9 is Relation-like Function-like Element of PFuncs (V,C)
dom v9 is set
{ H1(b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
r is 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 { H1(b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : S1[b1] } is set
r is Relation-like Function-like Element of PFuncs (V,C)
{ H1(b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : S2[b1] } 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

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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in u or not b1 tolerates b2 )
}
is set

{ b1 where b1 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)
{ H1(b1) where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : S2[b1] } is set
{ H1(b1) where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : S1[b1] } 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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in u or not b1 tolerates b2 )
}
is set

u ^ (V,C,u) is finite Element of Fin (PFuncs (V,C))
v is set
{ (b1 \/ b2) where b1, b2 is Relation-like Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in (V,C,u) & b1 tolerates b2 ) } 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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in u or not b1 tolerates b2 )
}
is set

v is Relation-like Function-like Element of PFuncs (V,C)
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : S1[b1] } 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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in u or not b1 tolerates b2 )
}
is set

v is set
r is Relation-like Function-like Element of PFuncs ((V,C,u),C)
[:V,C:] 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
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

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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in u or not b1 tolerates b2 )
}
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

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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in u or not b1 tolerates b2 )
}
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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,u),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in u or not b1 tolerates b2 )
}
is set

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

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)

{ (b1 \/ b2) where b1, b2 is Relation-like Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in r & b1 tolerates b2 ) } is set
dom w is set
(dom w) /\ (dom v) is set
pf is set
w . pf is set
v . pf is 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
{ H1(b1) where b1 is Element of v9 : S2[b1] } is set
{ (w . b1) where b1 is Element of [u] : verum } is set
pf is finite set

dom (v | pf) is finite set
a is set
SA is Element of [u]
w . SA is 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

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

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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in u } ) where b1 is Relation-like Function-like Element of PFuncs (u,v) : dom b1 = u } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in u } ) where b1 is Relation-like Function-like Element of PFuncs (u,v) : dom b1 = u } is set
{ (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in u } ) where b1 is Relation-like Function-like Element of PFuncs (u,v) : ( b1 in PFuncs (u,v) & dom b1 = u ) } is set
pf is set
sf is Relation-like Function-like Element of PFuncs (u,v)
{ ((sf . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
union { ((sf . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
dom sf is set
r is functional non empty finite set
{ ((a1 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
union { ((a1 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
{ H1(b1) where b1 is Relation-like Function-like Element of r : S1[b1] } 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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in u } ) where b1 is Relation-like Function-like Element of PFuncs (u,v) : dom b1 = u } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in u } ) where b1 is Relation-like Function-like Element of PFuncs (u,v) : dom b1 = u } is set

r is set
v9 is Relation-like Function-like Element of PFuncs (u,v)
{ ((v9 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
union { ((v9 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (C,u) : b2 in v } ) where b1 is Relation-like Function-like Element of PFuncs (v,r) : dom b1 = v } is set
(PFuncs (C,u)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (C,u) : b2 in v } ) where b1 is Relation-like Function-like Element of PFuncs (v,r) : dom b1 = 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

{ ((sf . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (C,u) : b1 in v } is set
union { ((sf . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (C,u) : b1 in v } is set
dom sf is finite Element of bool v

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

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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in u } ) where b1 is Relation-like Function-like Element of PFuncs (u,u) : dom b1 = u } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in u } ) where b1 is Relation-like Function-like Element of PFuncs (u,u) : dom b1 = u } is set
{ ((a1 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
union { ((a1 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set

v is Relation-like Function-like Element of PFuncs (u,u)
dom v is set
{ {} where b1 is Relation-like Function-like Element of PFuncs (u,u) : S1[b1] } is set
v is Relation-like Function-like Element of PFuncs (u,u)
{ ((v . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 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 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
union { ((v . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in u } is set
{ H2(b1) where b1 is Relation-like Function-like Element of PFuncs (u,u) : S1[b1] } is set
{ H1(b1) where b1 is Relation-like Function-like Element of PFuncs (u,u) : S1[b1] } is set
[:V,C:] 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
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

V is set
C is finite set

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

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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,v9),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in v9 or not b1 tolerates b2 )
}
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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,v9),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in v9 or not b1 tolerates b2 )
}
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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in v9 } ) where b1 is Relation-like Function-like Element of PFuncs (v9,w) : dom b1 = v9 } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in v9 } ) where b1 is Relation-like Function-like Element of PFuncs (v9,w) : dom b1 = 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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in sf } ) where b1 is Relation-like Function-like Element of PFuncs (sf,a) : dom b1 = sf } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in sf } ) where b1 is Relation-like Function-like Element of PFuncs (sf,a) : dom b1 = 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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in w } ) where b1 is Relation-like Function-like Element of PFuncs (w,pf) : dom b1 = w } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in w } ) where b1 is Relation-like Function-like Element of PFuncs (w,pf) : dom b1 = 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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in w } ) where b1 is Relation-like Function-like Element of PFuncs (w,pf) : dom b1 = w } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in w } ) where b1 is Relation-like Function-like Element of PFuncs (w,pf) : dom b1 = 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))

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)

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

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

(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

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

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

r is finite Element of Fin (PFuncs (V,C))
{ H1(b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : ( H1(b1) in u & S2[b1] ) } 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)
{ H3(b1,b2) where b1, b2 is Relation-like Function-like Element of PFuncs (V,C) : S3[b1,b2] } is set
{ H3(b1,b2) where b1, b2 is Relation-like Function-like Element of PFuncs (V,C) : S4[b1,b2] } 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)
{ H4(b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : S5[b1] } is set
{ H4(b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : S1[b1] } is set
{ H2(b1,b2) where b1, b2 is Relation-like Function-like Element of PFuncs (V,C) : ( b2 = v & S6[b1,b2] ) } is set
{ H2(b1,v) where b1 is Relation-like Function-like Element of PFuncs (V,C) : S6[b1,v] } is set
{ (b1 \/ v) where b1 is Relation-like Function-like Element of PFuncs (V,C) : ( not b1 tolerates v & b1 in u & b1 tolerates v ) } is set
sf is set
a is Relation-like Function-like Element of PFuncs (V,C)

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

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

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

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

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

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

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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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

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

(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))
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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)

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

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

(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

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

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

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

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

v is set
V is set
C is finite set

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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,r),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in r or not b1 tolerates b2 )
}
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

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

(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

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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in v } ) where b1 is Relation-like Function-like Element of PFuncs (v,r) : dom b1 = v } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in v } ) where b1 is Relation-like Function-like Element of PFuncs (v,r) : dom b1 = v } is set

the carrier of (SubstLatt (V,C)) is non empty set
w is Relation-like Function-like Element of PFuncs (V,C)

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

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

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

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 . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 in v9 } is set
union { ((a . b1) \ b1) where b1 is Relation-like Function-like Element of PFuncs (V,C) : b1 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

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

(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
{ (b1 \/ b2) where b1, b2 is Relation-like Function-like Element of PFuncs (V,C) : ( b1 in v9 & b2 in pf & b1 tolerates b2 ) } 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 { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in v9 } ) where b1 is Relation-like Function-like Element of PFuncs (v9,w) : dom b1 = v9 } is set
(PFuncs (V,C)) /\ { (union { ((b1 . b2) \ b2) where b2 is Relation-like Function-like Element of PFuncs (V,C) : b2 in v9 } ) where b1 is Relation-like Function-like Element of PFuncs (v9,w) : dom b1 = 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

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
H1(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
{ b1 where b1 is Relation-like Function-like Element of PFuncs ((V,C,v),C) : for b2 being Relation-like Function-like Element of PFuncs (V,C) holds
( not b2 in v or not b1 tolerates b2 )
}
is set

mi (V,C,v) is functional finite Element of SubstitutionSet (V,C)
H1(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

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