( 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 ; :: thesis: ( 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; :: thesis: A is 4,1 integer
thus A is 4,1 integer by A1, A10, A9, Th58, XBOOLE_1:79; :: thesis: verum