consider S being non empty non void 1-1-connectives 10 -connectives strict bool-correct 4,1 integer BoolSignature such that

A1: ( the carrier of S = {0,1} & ex I being SortSymbol of S st

( I = 1 & the connectives of S . 4 is_of_type {} ,I ) ) by Th47;

consider C being non empty non void strict 4 -connectives ConnectivesSignature such that

A2: ( C is 1,1,1 -array & C is 1-1-connectives & the carrier of S c= the carrier of C & the carrier' of S misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin {0,1} ) by A1, Th52;

take G = S +* C; :: thesis: ( G is 1-1-connectives & G is 14 -connectives & G is 11,1,1 -array & G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

A3: the connectives of G = the connectives of S ^ the connectives of C by Def52;

A4: the ResultSort of G = the ResultSort of S +* the ResultSort of C by Th51;

( rng the connectives of S c= the carrier' of S & rng the connectives of C c= the carrier' of C ) by RELAT_1:def 19;

hence the connectives of G is one-to-one by A3, A2, XBOOLE_1:64, FINSEQ_3:91; :: according to AOFA_A00:def 28 :: thesis: ( G is 14 -connectives & G is 11,1,1 -array & G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

thus G is 14 -connectives ; :: thesis: ( G is 11,1,1 -array & G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

( 10 + 1 = 11 & 1 > 0 ) ;

hence G is 11,1,1 -array by A2, Th53; :: thesis: ( G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

the bool-sort of G = the bool-sort of S by Def52;

then A5: the bool-sort of G in {0,1} by A1;

1 + 3 <= len the connectives of C by A2;

then 2 <= len the connectives of C by XXREAL_0:2;

then ( 2 in dom the connectives of C & len the connectives of S = 10 ) by Def29, FINSEQ_3:25;

then ( the connectives of C . (1 + 1) = the connectives of G . (10 + (1 + 1)) & the connectives of C . (1 + 1) in the carrier' of C & dom the ResultSort of C = the carrier' of C ) by A3, FUNCT_1:102, FINSEQ_1:def 7, FUNCT_2:def 1;

hence the ResultSort of G . ( the connectives of G . (11 + 1)) <> the bool-sort of G by A2, A5, A4, FUNCT_4:13; :: according to AOFA_A00:def 53 :: thesis: ( G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

thus G is 4,1 integer by A2, Th54; :: thesis: ( G is bool-correct & not G is empty & not G is void )

thus G is bool-correct by A2, Th55; :: thesis: ( not G is empty & not G is void )

thus ( not G is empty & not G is void ) ; :: thesis: verum

A1: ( the carrier of S = {0,1} & ex I being SortSymbol of S st

( I = 1 & the connectives of S . 4 is_of_type {} ,I ) ) by Th47;

consider C being non empty non void strict 4 -connectives ConnectivesSignature such that

A2: ( C is 1,1,1 -array & C is 1-1-connectives & the carrier of S c= the carrier of C & the carrier' of S misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin {0,1} ) by A1, Th52;

take G = S +* C; :: thesis: ( G is 1-1-connectives & G is 14 -connectives & G is 11,1,1 -array & G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

A3: the connectives of G = the connectives of S ^ the connectives of C by Def52;

A4: the ResultSort of G = the ResultSort of S +* the ResultSort of C by Th51;

( rng the connectives of S c= the carrier' of S & rng the connectives of C c= the carrier' of C ) by RELAT_1:def 19;

hence the connectives of G is one-to-one by A3, A2, XBOOLE_1:64, FINSEQ_3:91; :: according to AOFA_A00:def 28 :: thesis: ( G is 14 -connectives & G is 11,1,1 -array & G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

thus G is 14 -connectives ; :: thesis: ( G is 11,1,1 -array & G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

( 10 + 1 = 11 & 1 > 0 ) ;

hence G is 11,1,1 -array by A2, Th53; :: thesis: ( G is 11 array-correct & G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

the bool-sort of G = the bool-sort of S by Def52;

then A5: the bool-sort of G in {0,1} by A1;

1 + 3 <= len the connectives of C by A2;

then 2 <= len the connectives of C by XXREAL_0:2;

then ( 2 in dom the connectives of C & len the connectives of S = 10 ) by Def29, FINSEQ_3:25;

then ( the connectives of C . (1 + 1) = the connectives of G . (10 + (1 + 1)) & the connectives of C . (1 + 1) in the carrier' of C & dom the ResultSort of C = the carrier' of C ) by A3, FUNCT_1:102, FINSEQ_1:def 7, FUNCT_2:def 1;

hence the ResultSort of G . ( the connectives of G . (11 + 1)) <> the bool-sort of G by A2, A5, A4, FUNCT_4:13; :: according to AOFA_A00:def 53 :: thesis: ( G is 4,1 integer & G is bool-correct & not G is empty & not G is void )

thus G is 4,1 integer by A2, Th54; :: thesis: ( G is bool-correct & not G is empty & not G is void )

thus G is bool-correct by A2, Th55; :: thesis: ( not G is empty & not G is void )

thus ( not G is empty & not G is void ) ; :: thesis: verum