:: BVFUNC24 semantic presentation

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

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

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

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

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

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

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

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

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

theorem Th10: :: BVFUNC24:10
for b1, b2, b3, b4, b5, b6, b7 being set
for b8 being Function
for b9, b10, b11, b12, b13, b14, b15 being set st b8 = ((((((b2 .--> b10) +* (b3 .--> b11)) +* (b4 .--> b12)) +* (b5 .--> b13)) +* (b6 .--> b14)) +* (b7 .--> b15)) +* (b1 .--> b9) holds
rng b8 = {(b8 . b1),(b8 . b2),(b8 . b3),(b8 . b4),(b8 . b5),(b8 . b6),(b8 . b7)}
proof end;

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

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

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

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

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

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

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

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

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

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

theorem Th21: :: BVFUNC24:21
for b1, b2, b3, b4, b5, b6, b7, b8 being set
for b9 being Function
for b10, b11, b12, b13, b14, b15, b16, b17 being set st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & b1 <> b8 & b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> 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 & b9 = (((((((b2 .--> b11) +* (b3 .--> b12)) +* (b4 .--> b13)) +* (b5 .--> b14)) +* (b6 .--> b15)) +* (b7 .--> b16)) +* (b8 .--> b17)) +* (b1 .--> b10) holds
( b9 . b2 = b11 & b9 . b3 = b12 & b9 . b4 = b13 & b9 . b5 = b14 & b9 . b6 = b15 & b9 . b7 = b16 )
proof end;

theorem Th22: :: BVFUNC24:22
for b1, b2, b3, b4, b5, b6, b7, b8 being set
for b9 being Function
for b10, b11, b12, b13, b14, b15, b16, b17 being set st b9 = (((((((b2 .--> b11) +* (b3 .--> b12)) +* (b4 .--> b13)) +* (b5 .--> b14)) +* (b6 .--> b15)) +* (b7 .--> b16)) +* (b8 .--> b17)) +* (b1 .--> b10) holds
dom b9 = {b1,b2,b3,b4,b5,b6,b7,b8}
proof end;

theorem Th23: :: BVFUNC24:23
for b1, b2, b3, b4, b5, b6, b7, b8 being set
for b9 being Function
for b10, b11, b12, b13, b14, b15, b16, b17 being set st b9 = (((((((b2 .--> b11) +* (b3 .--> b12)) +* (b4 .--> b13)) +* (b5 .--> b14)) +* (b6 .--> b15)) +* (b7 .--> b16)) +* (b8 .--> b17)) +* (b1 .--> b10) holds
rng b9 = {(b9 . b1),(b9 . b2),(b9 . b3),(b9 . b4),(b9 . b5),(b9 . b6),(b9 . b7),(b9 . b8)}
proof end;

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

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

Lemma20: for b1, b2, b3 being set holds
( b1 in union {b2,{b3}} iff ( b1 in b2 or b1 = b3 ) )
proof end;

definition
let c1, c2, c3, c4, c5, c6, c7, c8, c9 be set ;
func {c1,c2,c3,c4,c5,c6,c7,c8,c9} -> set means :Def1: :: BVFUNC24:def 1
for b1 being set holds
( b1 in a10 iff ( b1 = a1 or b1 = a2 or b1 = a3 or b1 = a4 or b1 = a5 or b1 = a6 or b1 = a7 or b1 = a8 or b1 = a9 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 = c1 or b2 = c2 or b2 = c3 or b2 = c4 or b2 = c5 or b2 = c6 or b2 = c7 or b2 = c8 or b2 = c9 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 = c1 or b3 = c2 or b3 = c3 or b3 = c4 or b3 = c5 or b3 = c6 or b3 = c7 or b3 = c8 or b3 = c9 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 = c1 or b3 = c2 or b3 = c3 or b3 = c4 or b3 = c5 or b3 = c6 or b3 = c7 or b3 = c8 or b3 = c9 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines { BVFUNC24:def 1 :
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being set holds
( b10 = {b1,b2,b3,b4,b5,b6,b7,b8,b9} iff for b11 being set holds
( b11 in b10 iff ( b11 = b1 or b11 = b2 or b11 = b3 or b11 = b4 or b11 = b5 or b11 = b6 or b11 = b7 or b11 = b8 or b11 = b9 ) ) );

Lemma22: for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2,b3,b4} \/ {b5,b6,b7,b8,b9}
proof end;

theorem Th26: :: BVFUNC24:26
canceled;

theorem Th27: :: BVFUNC24:27
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1} \/ {b2,b3,b4,b5,b6,b7,b8,b9}
proof end;

theorem Th28: :: BVFUNC24:28
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2} \/ {b3,b4,b5,b6,b7,b8,b9}
proof end;

theorem Th29: :: BVFUNC24:29
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2,b3} \/ {b4,b5,b6,b7,b8,b9}
proof end;

theorem Th30: :: BVFUNC24:30
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2,b3,b4} \/ {b5,b6,b7,b8,b9} by Lemma22;

theorem Th31: :: BVFUNC24:31
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2,b3,b4,b5} \/ {b6,b7,b8,b9}
proof end;

theorem Th32: :: BVFUNC24:32
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2,b3,b4,b5,b6} \/ {b7,b8,b9}
proof end;

theorem Th33: :: BVFUNC24:33
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2,b3,b4,b5,b6,b7} \/ {b8,b9}
proof end;

theorem Th34: :: BVFUNC24:34
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set holds {b1,b2,b3,b4,b5,b6,b7,b8,b9} = {b1,b2,b3,b4,b5,b6,b7,b8} \/ {b9}
proof end;

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

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

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

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

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

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

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

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

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

theorem Th44: :: BVFUNC24:44
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set
for b10 being Function
for b11, b12, b13, b14, b15, b16, b17, b18, b19 being set st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & b1 <> b8 & b1 <> b9 & b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & b2 <> b9 & b3 <> b4 & b3 <> b5 & b3 <> b6 & b3 <> b7 & b3 <> b8 & b3 <> b9 & b4 <> b5 & b4 <> b6 & b4 <> b7 & b4 <> b8 & b4 <> b9 & b5 <> b6 & b5 <> b7 & b5 <> b8 & b5 <> b9 & b6 <> b7 & b6 <> b8 & b6 <> b9 & b7 <> b8 & b7 <> b9 & b8 <> b9 & b10 = ((((((((b2 .--> b12) +* (b3 .--> b13)) +* (b4 .--> b14)) +* (b5 .--> b15)) +* (b6 .--> b16)) +* (b7 .--> b17)) +* (b8 .--> b18)) +* (b9 .--> b19)) +* (b1 .--> b11) holds
( b10 . b1 = b11 & b10 . b2 = b12 & b10 . b3 = b13 & b10 . b4 = b14 & b10 . b5 = b15 & b10 . b6 = b16 & b10 . b7 = b17 & b10 . b8 = b18 & b10 . b9 = b19 )
proof end;

theorem Th45: :: BVFUNC24:45
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set
for b10 being Function
for b11, b12, b13, b14, b15, b16, b17, b18, b19 being set st b10 = ((((((((b2 .--> b12) +* (b3 .--> b13)) +* (b4 .--> b14)) +* (b5 .--> b15)) +* (b6 .--> b16)) +* (b7 .--> b17)) +* (b8 .--> b18)) +* (b9 .--> b19)) +* (b1 .--> b11) holds
dom b10 = {b1,b2,b3,b4,b5,b6,b7,b8,b9}
proof end;

theorem Th46: :: BVFUNC24:46
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set
for b10 being Function
for b11, b12, b13, b14, b15, b16, b17, b18, b19 being set st b10 = ((((((((b2 .--> b12) +* (b3 .--> b13)) +* (b4 .--> b14)) +* (b5 .--> b15)) +* (b6 .--> b16)) +* (b7 .--> b17)) +* (b8 .--> b18)) +* (b9 .--> b19)) +* (b1 .--> b11) holds
rng b10 = {(b10 . b1),(b10 . b2),(b10 . b3),(b10 . b4),(b10 . b5),(b10 . b6),(b10 . b7),(b10 . b8),(b10 . b9)}
proof end;

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

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