set X = {0,1};

set Y = {0,1,2,3,4,5,6,7,8,9};

reconsider 00 = 0 , x1 = 1 as Element of {0,1} by TARSKI:def 2;

reconsider y0 = 0 , 01 = 1, 02 = 2, 03 = 3, 04 = 4, 05 = 5, 06 = 6, 07 = 7, 08 = 8, 09 = 9 as Element of {0,1,2,3,4,5,6,7,8,9} by ENUMSET1:def 8;

set aa = <*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>;

set a = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {});

set r = ({0,1,2,9} --> 00) \/ ({3,4,5,6,7,8} --> x1);

( <*00*> in {0,1} * & <*00,00*> in {0,1} * & <*x1*> in {0,1} * & <*x1,x1*> in {0,1} * & <*> {0,1} in {0,1} * ) by FINSEQ_1:def 11;

then A1: ( {{},<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} c= {0,1} * & rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= (rng (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>)) \/ (rng ({0} --> {})) & dom ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) = (dom (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>)) \/ (dom ({0} --> {})) & dom ({0} --> {}) = {0} & rng ({0} --> {}) = {{}} ) by Th10, FUNCT_4:17, FUNCT_4:def 1;

then rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} \/ {{}} by Th21;

then ( rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {{},<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} & dom (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) = Seg 9 ) by Th12, FINSEQ_1:89;

then ( rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {0,1} * & dom ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) = {0,1,2,3,4,5,6,7,8,9} ) by A1, Th12, Th22;

then reconsider a = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {}) as Function of {0,1,2,3,4,5,6,7,8,9},({0,1} *) by FUNCT_2:2;

A2: ( dom ({0,1,2,9} --> 00) = {0,1,2,9} & dom ({3,4,5,6,7,8} --> x1) = {3,4,5,6,7,8} ) ;

{0,1,2,9} misses {3,4,5,6,7,8}

A4: dom r = {0,1,2,9} \/ {3,4,5,6,7,8} by A2, XTUPLE_0:23

.= ({0,1,2} \/ {9}) \/ {3,4,5,6,7,8} by ENUMSET1:6

.= ({0,1,2} \/ {3,4,5,6,7,8}) \/ {9} by XBOOLE_1:4

.= {0,1,2,3,4,5,6,7,8} \/ {9} by Th13

.= {0,1,2,3,4,5,6,7,8,9} by ENUMSET1:85 ;

rng r = (rng ({0,1,2,9} --> 00)) \/ (rng ({3,4,5,6,7,8} --> x1)) by RELAT_1:12

.= {00} \/ (rng ({3,4,5,6,7,8} --> x1))

.= {00} \/ {x1}

.= {0,1} by ENUMSET1:1 ;

then reconsider r = r as Function of {0,1,2,3,4,5,6,7,8,9},{0,1} by A4, FUNCT_2:2;

set B = BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #);

A5: len the connectives of BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) = (len <*y0,01,02,03,04,05,06,07*>) + (len <*08,09*>) by FINSEQ_1:22

.= 8 + (len <*08,09*>) by Th19

.= 8 + 2 by FINSEQ_1:44

.= 10 ;

( BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is 10 -connectives & not BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is empty & not BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is void ) by A5;

then reconsider B = BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) as non empty non void 10 -connectives strict BoolSignature ;

take B ; :: thesis: ( B is 1-1-connectives & B is 4,1 integer & B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

thus the connectives of B is one-to-one :: according to AOFA_A00:def 28 :: thesis: ( B is 4,1 integer & B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

A16: ( the connectives of B . 1 = 0 & 0 in {0} ) by Th25, TARSKI:def 1;

hence the Arity of B . ( the connectives of B . 1) = ({0} --> {}) . 0 by A1, FUNCT_4:13

.= {} ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( 0 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;

then [0, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [0, the bool-sort of B] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B by A16, FUNCT_1:1; :: thesis: ( the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

A17: ( the connectives of B . 2 = 1 & 1 nin {0} ) by Th25, TARSKI:def 1;

hence the Arity of B . ( the connectives of B . 2) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 1 by A1, FUNCT_4:11

.= <* the bool-sort of B*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( 1 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;

then [1, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [1, the bool-sort of B] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B by A17, FUNCT_1:1; :: thesis: ( the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

A18: ( the connectives of B . 3 = 2 & 2 nin {0} ) by Th25, TARSKI:def 1;

hence the Arity of B . ( the connectives of B . 3) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 2 by A1, FUNCT_4:11

.= <* the bool-sort of B, the bool-sort of B*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( 2 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;

then [2, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [2, the bool-sort of B] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B by A18, FUNCT_1:1; :: thesis: ( the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

thus the carrier of B = {0,1} ; :: thesis: ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I )

reconsider I = 1 as SortSymbol of B ;

take I ; :: thesis: ( I = 1 & the connectives of B . 4 is_of_type {} ,I )

thus I = 1 ; :: thesis: the connectives of B . 4 is_of_type {} ,I

A19: ( the connectives of B . 4 = 3 & 3 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . 4) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 3 by FUNCT_4:11

.= {} by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: the ResultSort of B . ( the connectives of B . 4) = I

( 3 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [3,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [3,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 4) = I by A19, FUNCT_1:1; :: thesis: verum

set Y = {0,1,2,3,4,5,6,7,8,9};

reconsider 00 = 0 , x1 = 1 as Element of {0,1} by TARSKI:def 2;

reconsider y0 = 0 , 01 = 1, 02 = 2, 03 = 3, 04 = 4, 05 = 5, 06 = 6, 07 = 7, 08 = 8, 09 = 9 as Element of {0,1,2,3,4,5,6,7,8,9} by ENUMSET1:def 8;

set aa = <*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>;

set a = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {});

set r = ({0,1,2,9} --> 00) \/ ({3,4,5,6,7,8} --> x1);

( <*00*> in {0,1} * & <*00,00*> in {0,1} * & <*x1*> in {0,1} * & <*x1,x1*> in {0,1} * & <*> {0,1} in {0,1} * ) by FINSEQ_1:def 11;

then A1: ( {{},<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} c= {0,1} * & rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= (rng (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>)) \/ (rng ({0} --> {})) & dom ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) = (dom (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>)) \/ (dom ({0} --> {})) & dom ({0} --> {}) = {0} & rng ({0} --> {}) = {{}} ) by Th10, FUNCT_4:17, FUNCT_4:def 1;

then rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} \/ {{}} by Th21;

then ( rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {{},<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>} & dom (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) = Seg 9 ) by Th12, FINSEQ_1:89;

then ( rng ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) c= {0,1} * & dom ((<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {})) = {0,1,2,3,4,5,6,7,8,9} ) by A1, Th12, Th22;

then reconsider a = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) +* ({0} --> {}) as Function of {0,1,2,3,4,5,6,7,8,9},({0,1} *) by FUNCT_2:2;

A2: ( dom ({0,1,2,9} --> 00) = {0,1,2,9} & dom ({3,4,5,6,7,8} --> x1) = {3,4,5,6,7,8} ) ;

{0,1,2,9} misses {3,4,5,6,7,8}

proof

then reconsider r = ({0,1,2,9} --> 00) \/ ({3,4,5,6,7,8} --> x1) as Function by A2, GRFUNC_1:13;
assume
{0,1,2,9} meets {3,4,5,6,7,8}
; :: thesis: contradiction

then consider x being object such that

A3: ( x in {0,1,2,9} & x in {3,4,5,6,7,8} ) by XBOOLE_0:3;

( ( x = 0 or x = 1 or x = 2 or x = 9 ) & ( x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 ) ) by A3, ENUMSET1:def 2, ENUMSET1:def 4;

hence contradiction ; :: thesis: verum

end;then consider x being object such that

A3: ( x in {0,1,2,9} & x in {3,4,5,6,7,8} ) by XBOOLE_0:3;

( ( x = 0 or x = 1 or x = 2 or x = 9 ) & ( x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 ) ) by A3, ENUMSET1:def 2, ENUMSET1:def 4;

hence contradiction ; :: thesis: verum

A4: dom r = {0,1,2,9} \/ {3,4,5,6,7,8} by A2, XTUPLE_0:23

.= ({0,1,2} \/ {9}) \/ {3,4,5,6,7,8} by ENUMSET1:6

.= ({0,1,2} \/ {3,4,5,6,7,8}) \/ {9} by XBOOLE_1:4

.= {0,1,2,3,4,5,6,7,8} \/ {9} by Th13

.= {0,1,2,3,4,5,6,7,8,9} by ENUMSET1:85 ;

rng r = (rng ({0,1,2,9} --> 00)) \/ (rng ({3,4,5,6,7,8} --> x1)) by RELAT_1:12

.= {00} \/ (rng ({3,4,5,6,7,8} --> x1))

.= {00} \/ {x1}

.= {0,1} by ENUMSET1:1 ;

then reconsider r = r as Function of {0,1,2,3,4,5,6,7,8,9},{0,1} by A4, FUNCT_2:2;

set B = BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #);

A5: len the connectives of BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) = (len <*y0,01,02,03,04,05,06,07*>) + (len <*08,09*>) by FINSEQ_1:22

.= 8 + (len <*08,09*>) by Th19

.= 8 + 2 by FINSEQ_1:44

.= 10 ;

( BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is 10 -connectives & not BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is empty & not BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) is void ) by A5;

then reconsider B = BoolSignature(# {0,1},{0,1,2,3,4,5,6,7,8,9},a,r,00,(<*y0,01,02,03,04,05,06,07*> ^ <*08,09*>) #) as non empty non void 10 -connectives strict BoolSignature ;

take B ; :: thesis: ( B is 1-1-connectives & B is 4,1 integer & B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

thus the connectives of B is one-to-one :: according to AOFA_A00:def 28 :: thesis: ( B is 4,1 integer & B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

proof

thus
B is 4,1 integer
:: thesis: ( B is bool-correct & the carrier of B = {0,1} & ex I being SortSymbol of B st
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 the connectives of B or not y in proj1 the connectives of B or not the connectives of B . x = the connectives of B . y or x = y )

assume A6: ( x in dom the connectives of B & y in dom the connectives of B ) ; :: thesis: ( not the connectives of B . x = the connectives of B . y or x = y )

set c = the connectives of B;

A7: dom the connectives of B = Seg 10 by Th25;

A8: ( y = 1 or y = 2 or y = 3 or y = 4 or y = 5 or y = 6 or y = 7 or y = 8 or y = 9 or y = 10 ) by A6, A7, Th23, ENUMSET1:def 8;

( the connectives of B . 1 = y0 & the connectives of B . 2 = 01 & the connectives of B . 3 = 02 & the connectives of B . 4 = 03 & the connectives of B . 5 = 04 & the connectives of B . 6 = 05 & the connectives of B . 7 = 06 & the connectives of B . 8 = 07 & the connectives of B . 9 = 08 & the connectives of B . 10 = 09 ) by Th25;

hence ( not the connectives of B . x = the connectives of B . y or x = y ) by A7, A8, A6, Th23, ENUMSET1:def 8; :: thesis: verum

end;assume A6: ( x in dom the connectives of B & y in dom the connectives of B ) ; :: thesis: ( not the connectives of B . x = the connectives of B . y or x = y )

set c = the connectives of B;

A7: dom the connectives of B = Seg 10 by Th25;

A8: ( y = 1 or y = 2 or y = 3 or y = 4 or y = 5 or y = 6 or y = 7 or y = 8 or y = 9 or y = 10 ) by A6, A7, Th23, ENUMSET1:def 8;

( the connectives of B . 1 = y0 & the connectives of B . 2 = 01 & the connectives of B . 3 = 02 & the connectives of B . 4 = 03 & the connectives of B . 5 = 04 & the connectives of B . 6 = 05 & the connectives of B . 7 = 06 & the connectives of B . 8 = 07 & the connectives of B . 9 = 08 & the connectives of B . 10 = 09 ) by Th25;

hence ( not the connectives of B . x = the connectives of B . y or x = y ) by A7, A8, A6, Th23, ENUMSET1:def 8; :: thesis: verum

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

proof

thus
len the connectives of B >= 3
by A5; :: according to AOFA_A00:def 30 :: thesis: ( the connectives of B . 1 is_of_type {} , the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st
thus
len the connectives of B >= 4 + 6
by A5; :: according to AOFA_A00:def 38 :: thesis: ex I being Element of B st

( I = 1 & I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

reconsider I = x1 as Element of B ;

take I ; :: thesis: ( I = 1 & I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus I = 1 ; :: thesis: ( I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus I <> the bool-sort of B ; :: thesis: ( the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A9: ( the connectives of B . 4 = 3 & 3 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . 4) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 3 by FUNCT_4:11

.= {} by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 4) = I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 3 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [3,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [3,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 4) = I by A9, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A10: ( the connectives of B . 5 = 4 & 4 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 1)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 4 by FUNCT_4:11

.= {} by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 1)) = I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 4 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [4,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [4,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 1)) = I by A10, FUNCT_1:1; :: thesis: ( the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . 4 <> the connectives of B . (4 + 1) by A9, Th25; :: thesis: ( the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A11: ( the connectives of B . 6 = 5 & 5 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 2)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 5 by FUNCT_4:11

.= <*I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 2)) = I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 5 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [5,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [5,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 2)) = I by A11, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A12: ( the connectives of B . 7 = 6 & 6 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 3)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 6 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 3)) = I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 6 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [6,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [6,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 3)) = I by A12, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A13: ( the connectives of B . 8 = 7 & 7 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 4)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 7 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 4)) = I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 7 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [7,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [7,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 4)) = I by A13, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A14: ( the connectives of B . 9 = 8 & 8 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 5)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 8 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 5)) = I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 8 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [8,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [8,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 5)) = I by A14, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) by A13, Th25; :: thesis: ( the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) by A14, Th25; :: thesis: ( the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) by A14, Th25; :: thesis: the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B

A15: ( the connectives of B . 10 = 9 & 9 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 6)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 9 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: the ResultSort of B . ( the connectives of B . (4 + 6)) = the bool-sort of B

( 9 in {0,1,2,9} & the bool-sort of B in { the bool-sort of B} ) by TARSKI:def 1, ENUMSET1:def 2;

then [9,00] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [9,00] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 6)) = the bool-sort of B by A15, FUNCT_1:1; :: thesis: verum

end;( I = 1 & I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

reconsider I = x1 as Element of B ;

take I ; :: thesis: ( I = 1 & I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus I = 1 ; :: thesis: ( I <> the bool-sort of B & the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus I <> the bool-sort of B ; :: thesis: ( the connectives of B . 4 is_of_type {} ,I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A9: ( the connectives of B . 4 = 3 & 3 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . 4) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 3 by FUNCT_4:11

.= {} by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 4) = I & the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 3 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [3,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [3,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 4) = I by A9, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 1) is_of_type {} ,I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A10: ( the connectives of B . 5 = 4 & 4 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 1)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 4 by FUNCT_4:11

.= {} by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 1)) = I & the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 4 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [4,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [4,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 1)) = I by A10, FUNCT_1:1; :: thesis: ( the connectives of B . 4 <> the connectives of B . (4 + 1) & the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . 4 <> the connectives of B . (4 + 1) by A9, Th25; :: thesis: ( the connectives of B . (4 + 2) is_of_type <*I*>,I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A11: ( the connectives of B . 6 = 5 & 5 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 2)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 5 by FUNCT_4:11

.= <*I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 2)) = I & the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 5 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [5,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [5,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 2)) = I by A11, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 3) is_of_type <*I,I*>,I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A12: ( the connectives of B . 7 = 6 & 6 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 3)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 6 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 3)) = I & the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 6 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [6,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [6,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 3)) = I by A12, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 4) is_of_type <*I,I*>,I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A13: ( the connectives of B . 8 = 7 & 7 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 4)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 7 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 4)) = I & the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 7 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [7,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [7,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 4)) = I by A13, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 5) is_of_type <*I,I*>,I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

A14: ( the connectives of B . 9 = 8 & 8 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 5)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 8 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . (4 + 5)) = I & the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

( 8 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [8,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [8,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 5)) = I by A14, FUNCT_1:1; :: thesis: ( the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) & the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . (4 + 3) <> the connectives of B . (4 + 4) by A13, Th25; :: thesis: ( the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . (4 + 3) <> the connectives of B . (4 + 5) by A14, Th25; :: thesis: ( the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) & the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B )

thus the connectives of B . (4 + 4) <> the connectives of B . (4 + 5) by A14, Th25; :: thesis: the connectives of B . (4 + 6) is_of_type <*I,I*>, the bool-sort of B

A15: ( the connectives of B . 10 = 9 & 9 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . (4 + 6)) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 9 by FUNCT_4:11

.= <*I,I*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: the ResultSort of B . ( the connectives of B . (4 + 6)) = the bool-sort of B

( 9 in {0,1,2,9} & the bool-sort of B in { the bool-sort of B} ) by TARSKI:def 1, ENUMSET1:def 2;

then [9,00] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [9,00] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . (4 + 6)) = the bool-sort of B by A15, FUNCT_1:1; :: thesis: verum

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

A16: ( the connectives of B . 1 = 0 & 0 in {0} ) by Th25, TARSKI:def 1;

hence the Arity of B . ( the connectives of B . 1) = ({0} --> {}) . 0 by A1, FUNCT_4:13

.= {} ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( 0 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;

then [0, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [0, the bool-sort of B] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B by A16, FUNCT_1:1; :: thesis: ( the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

A17: ( the connectives of B . 2 = 1 & 1 nin {0} ) by Th25, TARSKI:def 1;

hence the Arity of B . ( the connectives of B . 2) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 1 by A1, FUNCT_4:11

.= <* the bool-sort of B*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( 1 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;

then [1, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [1, the bool-sort of B] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B by A17, FUNCT_1:1; :: thesis: ( the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

A18: ( the connectives of B . 3 = 2 & 2 nin {0} ) by Th25, TARSKI:def 1;

hence the Arity of B . ( the connectives of B . 3) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 2 by A1, FUNCT_4:11

.= <* the bool-sort of B, the bool-sort of B*> by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B & the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

( 2 in {0,1,2,9} & 00 in {00} ) by TARSKI:def 1, ENUMSET1:def 2;

then [2, the bool-sort of B] in {0,1,2,9} --> 00 by ZFMISC_1:87;

then [2, the bool-sort of B] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B by A18, FUNCT_1:1; :: thesis: ( the carrier of B = {0,1} & ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I ) )

thus the carrier of B = {0,1} ; :: thesis: ex I being SortSymbol of B st

( I = 1 & the connectives of B . 4 is_of_type {} ,I )

reconsider I = 1 as SortSymbol of B ;

take I ; :: thesis: ( I = 1 & the connectives of B . 4 is_of_type {} ,I )

thus I = 1 ; :: thesis: the connectives of B . 4 is_of_type {} ,I

A19: ( the connectives of B . 4 = 3 & 3 nin dom ({0} --> {}) ) by Th25;

hence the Arity of B . ( the connectives of B . 4) = (<*<*00*>,<*00,00*>,{},{},<*x1*>,<*x1,x1*>,<*x1,x1*>,<*x1,x1*>*> ^ <*<*x1,x1*>*>) . 3 by FUNCT_4:11

.= {} by Th24 ;

:: according to AOFA_A00:def 8 :: thesis: the ResultSort of B . ( the connectives of B . 4) = I

( 3 in {3,4,5,6,7,8} & I in {I} ) by TARSKI:def 1, ENUMSET1:def 4;

then [3,I] in {3,4,5,6,7,8} --> x1 by ZFMISC_1:87;

then [3,I] in r by XBOOLE_0:def 3;

hence the ResultSort of B . ( the connectives of B . 4) = I by A19, FUNCT_1:1; :: thesis: verum