:: BVFUNC23 semantic presentation

theorem Th1: :: BVFUNC23:1
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1 st b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 holds
CompF b3,b2 = (((b4 '/\' b5) '/\' b6) '/\' b7) '/\' b8
proof end;

theorem Th2: :: BVFUNC23:2
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1 st b2 is independent & b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 holds
CompF b4,b2 = (((b3 '/\' b5) '/\' b6) '/\' b7) '/\' b8
proof end;

theorem Th3: :: BVFUNC23:3
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1 st b2 is independent & b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 holds
CompF b5,b2 = (((b3 '/\' b4) '/\' b6) '/\' b7) '/\' b8
proof end;

theorem Th4: :: BVFUNC23:4
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1 st b2 is independent & b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 holds
CompF b6,b2 = (((b3 '/\' b4) '/\' b5) '/\' b7) '/\' b8
proof end;

theorem Th5: :: BVFUNC23:5
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1 st b2 is independent & b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 holds
CompF b7,b2 = (((b3 '/\' b4) '/\' b5) '/\' b6) '/\' b8
proof end;

theorem Th6: :: BVFUNC23:6
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1 st b2 is independent & b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 holds
CompF b8,b2 = (((b3 '/\' b4) '/\' b5) '/\' b6) '/\' b7
proof end;

theorem Th7: :: BVFUNC23:7
for b1, b2, b3, b4, b5, b6 being set
for b7 being Function
for b8, b9, b10, b11, b12, b13 being set st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b3 <> b4 & b3 <> b5 & b3 <> b6 & b4 <> b5 & b4 <> b6 & b5 <> b6 & b7 = (((((b2 .--> b9) +* (b3 .--> b10)) +* (b4 .--> b11)) +* (b5 .--> b12)) +* (b6 .--> b13)) +* (b1 .--> b8) holds
( b7 . b1 = b8 & b7 . b2 = b9 & b7 . b3 = b10 & b7 . b4 = b11 & b7 . b5 = b12 & b7 . b6 = b13 )
proof end;

theorem Th8: :: BVFUNC23:8
for b1, b2, b3, b4, b5, b6 being set
for b7 being Function
for b8, b9, b10, b11, b12, b13 being set st b7 = (((((b2 .--> b9) +* (b3 .--> b10)) +* (b4 .--> b11)) +* (b5 .--> b12)) +* (b6 .--> b13)) +* (b1 .--> b8) holds
dom b7 = {b1,b2,b3,b4,b5,b6}
proof end;

theorem Th9: :: BVFUNC23:9
for b1, b2, b3, b4, b5, b6 being set
for b7 being Function
for b8, b9, b10, b11, b12, b13 being set st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b3 <> b4 & b3 <> b5 & b3 <> b6 & b4 <> b5 & b4 <> b6 & b5 <> b6 & b7 = (((((b2 .--> b9) +* (b3 .--> b10)) +* (b4 .--> b11)) +* (b5 .--> b12)) +* (b6 .--> b13)) +* (b1 .--> b8) holds
rng b7 = {(b7 . b1),(b7 . b2),(b7 . b3),(b7 . b4),(b7 . b5),(b7 . b6)}
proof end;

theorem Th10: :: BVFUNC23:10
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1
for b9, b10 being Element of b1
for b11 being Function st b2 is independent & b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 holds
EqClass b10,((((b4 '/\' b5) '/\' b6) '/\' b7) '/\' b8) meets EqClass b9,b3
proof end;

theorem Th11: :: BVFUNC23:11
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1
for b9, b10 being Element of b1
for b11 being Function st b2 is independent & b2 = {b3,b4,b5,b6,b7,b8} & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b6 <> b7 & b6 <> b8 & b7 <> b8 & EqClass b9,(((b5 '/\' b6) '/\' b7) '/\' b8) = EqClass b10,(((b5 '/\' b6) '/\' b7) '/\' b8) holds
EqClass b10,(CompF b3,b2) meets EqClass b9,(CompF b4,b2)
proof end;