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; ( 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; AOFA_A00:def 28 ( 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
; ( 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; ( 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; AOFA_A00:def 53 ( 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; ( G is bool-correct & not G is empty & not G is void )
thus
G is bool-correct
by A2, Th55; ( not G is empty & not G is void )
thus
( not G is empty & not G is void )
; verum