( 11 = 10 + 1 & 4 + 6 <= 10 )
;
then consider B being non empty non void bool-correct BoolSignature , C being non empty non void ConnectivesSignature such that
A1:
( BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C & B is 10 -connectives & B is 4,1 integer & C is 1,1,1 -array & the carrier of B = the carrier of C & the carrier' of B = the carrier' of S \ (rng the connectives of C) & the carrier' of C = rng the connectives of C & the connectives of B = the connectives of S | 10 & the connectives of C = the connectives of S /^ 10 )
by Th63;
reconsider B = B as non empty non void bool-correct 4,1 integer BoolSignature by A1;
reconsider C = C as non empty non void 1,1,1 -array ConnectivesSignature by A1;
set s = the ResultSort of C . ( the connectives of C . 2);
1 + 3 <= len the connectives of C
by Def50;
then
2 <= len the connectives of C
by XXREAL_0:2;
then A2:
2 in dom the connectives of C
by FINSEQ_3:25;
then A3:
the ResultSort of C . ( the connectives of C . 2) in the carrier of B
by A1, FUNCT_1:102, FUNCT_2:5;
consider J, K, L being Element of C such that
A4:
( L = 1 & K = 1 & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )
by Def50;
A5:
the ResultSort of C . ( the connectives of C . 2) <> 1
by A4;
A6:
the connectives of S = the connectives of B ^ the connectives of C
by A1, Def52;
A7:
the ResultSort of S = the ResultSort of B +* the ResultSort of C
by A1, Th51;
A8:
the ResultSort of S . ( the connectives of S . (11 + 1)) <> the bool-sort of S
by Def53;
len the connectives of B = 10
by A1;
then
( the connectives of C . (1 + 1) = the connectives of S . (10 + (1 + 1)) & the connectives of C . (1 + 1) in the carrier' of C & dom the ResultSort of C = the carrier' of C )
by A6, A2, FUNCT_1:102, FINSEQ_1:def 7, FUNCT_2:def 1;
then
( the ResultSort of S . ( the connectives of S . (10 + (1 + 1))) = the ResultSort of C . ( the connectives of C . 2) & the bool-sort of B = the bool-sort of S )
by A1, Def52, A7, FUNCT_4:13;
then consider A1 being non-empty bool-correct MSAlgebra over B such that
A9:
( A1 is 4,1 integer & the Sorts of A1 . ( the ResultSort of C . ( the connectives of C . 2)) = INT ^omega )
by A3, A5, A8, Th64;
consider A2 being strict non-empty MSAlgebra over C such that
A10:
( A2 is 1,1,1 -array & the Sorts of A2 tolerates the Sorts of A1 )
by A9, Th56;
reconsider A = (B,A1) +* A2 as strict MSAlgebra over S by A1;
A11:
A is non-empty
;
(B,A1) +* A2 is bool-correct
by A10, Th57, A1, XBOOLE_1:79;
then
( the Sorts of ((B,A1) +* A2) . the bool-sort of S = BOOLEAN & (Den ((In (( the connectives of (B +* C) . 1), the carrier' of (B +* C))),((B,A1) +* A2))) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of (B +* C) . 2), the carrier' of (B +* C))),((B,A1) +* A2))) . <*x*> = 'not' x & (Den ((In (( the connectives of (B +* C) . 3), the carrier' of (B +* C))),((B,A1) +* A2))) . <*x,y*> = x '&' y ) ) )
by A1;
then
( the Sorts of A . the bool-sort of S = BOOLEAN & (Den ((In (( the connectives of S . 1), the carrier' of S)),A)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),A)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),A)) . <*x,y*> = x '&' y ) ) )
by A1;
then reconsider A = (B,A1) +* A2 as strict non-empty bool-correct MSAlgebra over S by A11, Def31;
take
A
; ( A is 11,1,1 -array & A is 4,1 integer )
11 = 10 + 1
;
hence
A is 11,1,1 -array
by A1, A10, Th59; A is 4,1 integer
thus
A is 4,1 integer
by A1, A10, A9, Th58, XBOOLE_1:79; verum