for b₁ being non empty set
for b₂ being Element of b₁
for b₃, b₄ being a_partition of b₁ holds EqClass b₂,(b₃ '/\' b₄) = (EqClass b₂,b₃) /\ (EqClass b₂,b₄)

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄ being a_partition of b₁ st b₂ = {b₃,b₄} & b₃ <> b₄ holds
'/\' b₂ = b₃ '/\' b₄

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅ being a_partition of b₁ st b₂ = {b₃,b₄,b₅} & b₃ <> b₄ & b₄ <> b₅ & b₅ <> b₃ holds
'/\' b₂ = (b₃ '/\' b₄) '/\' b₅

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅ being a_partition of b₁ st b₂ = {b₃,b₄,b₅} & b₃ <> b₄ & b₅ <> b₃ holds
CompF b₃,b₂ = b₄ '/\' b₅

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅ being a_partition of b₁ st b₂ = {b₃,b₄,b₅} & b₃ <> b₄ & b₄ <> b₅ holds
CompF b₄,b₂ = b₅ '/\' b₃

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅ being a_partition of b₁ st b₂ = {b₃,b₄,b₅} & b₄ <> b₅ & b₅ <> b₃ holds
CompF b₅,b₂ = b₃ '/\' b₄

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁ st b₂ = {b₃,b₄,b₅,b₆} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ holds
CompF b₃,b₂ = (b₄ '/\' b₅) '/\' b₆

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁ st b₂ = {b₃,b₄,b₅,b₆} & b₃ <> b₄ & b₄ <> b₅ & b₄ <> b₆ holds
CompF b₄,b₂ = (b₃ '/\' b₅) '/\' b₆

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁ st b₂ = {b₃,b₄,b₅,b₆} & b₃ <> b₅ & b₄ <> b₅ & b₅ <> b₆ holds
CompF b₅,b₂ = (b₃ '/\' b₄) '/\' b₆

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁ st b₂ = {b₃,b₄,b₅,b₆} & b₃ <> b₆ & b₄ <> b₆ & b₅ <> b₆ holds
CompF b₆,b₂ = (b₃ '/\' b₅) '/\' b₄

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds dom (((b₁ .--> b₄) +* (b₂ .--> b₅)) +* (b₃ .--> b₆)) = {b₁,b₂,b₃} by Lemma2;

for b₁ being Function
for b₂, b₃, b₄, b₅ being set st b₂ <> b₃ holds
((b₁ +* (b₂ .--> b₄)) +* (b₃ .--> b₅)) . b₂ = b₄ by Lemma3;

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> b₂ & b₃ <> b₁ holds
(((b₁ .--> b₄) +* (b₂ .--> b₅)) +* (b₃ .--> b₆)) . b₁ = b₄ by Lemma4;

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Function st b₇ = ((b₁ .--> b₄) +* (b₂ .--> b₅)) +* (b₃ .--> b₆) holds
rng b₇ = {(b₇ . b₁),(b₇ . b₂),(b₇ . b₃)} by Lemma5;

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁
for b₇ being Function
for b₈, b₉, b₁₀, b₁₁ being set st b₂ = {b₃,b₄,b₅,b₆} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₄ <> b₅ & b₄ <> b₆ & b₅ <> b₆ & b₇ = (((b₄ .--> b₉) +* (b₅ .--> b₁₀)) +* (b₆ .--> b₁₁)) +* (b₃ .--> b₈) holds
( b₇ . b₄ = b₉ & b₇ . b₅ = b₁₀ & b₇ . b₆ = b₁₁ )

for b₁, b₂, b₃, b₄ being set
for b₅ being Function
for b₆, b₇, b₈, b₉ being set st b₅ = (((b₂ .--> b₇) +* (b₃ .--> b₈)) +* (b₄ .--> b₉)) +* (b₁ .--> b₆) holds
dom b₅ = {b₁,b₂,b₃,b₄}

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁
for b₇ being Function
for b₈, b₉, b₁₀, b₁₁ being set st b₂ = {b₃,b₄,b₅,b₆} & b₇ = (((b₄ .--> b₉) +* (b₅ .--> b₁₀)) +* (b₆ .--> b₁₁)) +* (b₃ .--> b₈) holds
rng b₇ = {(b₇ . b₃),(b₇ . b₄),(b₇ . b₅),(b₇ . b₆)}

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁
for b₇, b₈ being Element of b₁
for b₉ being Function st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₄ <> b₅ & b₄ <> b₆ & b₅ <> b₆ holds
EqClass b₈,((b₄ '/\' b₅) '/\' b₆) meets EqClass b₇,b₃

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆ being a_partition of b₁
for b₇, b₈ being Element of b₁ st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₄ <> b₅ & b₄ <> b₆ & b₅ <> b₆ & EqClass b₇,(b₅ '/\' b₆) = EqClass b₈,(b₅ '/\' b₆) holds
EqClass b₈,(CompF b₃,b₂) meets EqClass b₇,(CompF b₄,b₂)

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅ being a_partition of b₁
for b₆, b₇ being Element of b₁ st b₂ is independent & b₂ = {b₃,b₄,b₅} & b₃ <> b₄ & b₄ <> b₅ & b₅ <> b₃ & EqClass b₆,b₅ = EqClass b₇,b₅ holds
EqClass b₇,(CompF b₃,b₂) meets EqClass b₆,(CompF b₄,b₂)

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆, b₇ being a_partition of b₁ st b₂ = {b₃,b₄,b₅,b₆,b₇} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₃ <> b₇ holds
CompF b₃,b₂ = ((b₄ '/\' b₅) '/\' b₆) '/\' b₇

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆, b₇ being a_partition of b₁ st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆,b₇} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₃ <> b₇ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ holds
CompF b₄,b₂ = ((b₃ '/\' b₅) '/\' b₆) '/\' b₇

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆, b₇ being a_partition of b₁ st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆,b₇} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₃ <> b₇ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ holds
CompF b₅,b₂ = ((b₃ '/\' b₄) '/\' b₆) '/\' b₇

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆, b₇ being a_partition of b₁ st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆,b₇} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₃ <> b₇ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ holds
CompF b₆,b₂ = ((b₃ '/\' b₄) '/\' b₅) '/\' b₇

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆, b₇ being a_partition of b₁ st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆,b₇} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₃ <> b₇ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ holds
CompF b₇,b₂ = ((b₃ '/\' b₄) '/\' b₅) '/\' b₆

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Function
for b₇, b₈, b₉, b₁₀, b₁₁ being set st b₁ <> b₂ & b₁ <> b₃ & b₁ <> b₄ & b₁ <> b₅ & b₂ <> b₃ & b₂ <> b₄ & b₂ <> b₅ & b₃ <> b₄ & b₃ <> b₅ & b₄ <> b₅ & b₆ = ((((b₂ .--> b₈) +* (b₃ .--> b₉)) +* (b₄ .--> b₁₀)) +* (b₅ .--> b₁₁)) +* (b₁ .--> b₇) holds
( b₆ . b₁ = b₇ & b₆ . b₂ = b₈ & b₆ . b₃ = b₉ & b₆ . b₄ = b₁₀ & b₆ . b₅ = b₁₁ )

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Function
for b₇, b₈, b₉, b₁₀, b₁₁ being set st b₆ = ((((b₂ .--> b₈) +* (b₃ .--> b₉)) +* (b₄ .--> b₁₀)) +* (b₅ .--> b₁₁)) +* (b₁ .--> b₇) holds
dom b₆ = {b₁,b₂,b₃,b₄,b₅}

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Function
for b₇, b₈, b₉, b₁₀, b₁₁ being set st b₆ = ((((b₂ .--> b₈) +* (b₃ .--> b₉)) +* (b₄ .--> b₁₀)) +* (b₅ .--> b₁₁)) +* (b₁ .--> b₇) holds
rng b₆ = {(b₆ . b₁),(b₆ . b₂),(b₆ . b₃),(b₆ . b₄),(b₆ . b₅)}

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆, b₇ being a_partition of b₁
for b₈, b₉ being Element of b₁
for b₁₀ being Function st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆,b₇} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₃ <> b₇ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ holds
EqClass b₉,(((b₄ '/\' b₅) '/\' b₆) '/\' b₇) meets EqClass b₈,b₃

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁)
for b₃, b₄, b₅, b₆, b₇ being a_partition of b₁
for b₈, b₉ being Element of b₁ st b₂ is independent & b₂ = {b₃,b₄,b₅,b₆,b₇} & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ & b₃ <> b₇ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ & EqClass b₈,((b₅ '/\' b₆) '/\' b₇) = EqClass b₉,((b₅ '/\' b₆) '/\' b₇) holds
EqClass b₉,(CompF b₃,b₂) meets EqClass b₈,(CompF b₄,b₂)