let s, I be set ; :: thesis: for S being non empty non void bool-correct BoolSignature st S is 4,I integer holds
for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )
let S be non empty non void bool-correct BoolSignature ; :: thesis: ( S is 4,I integer implies for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A1: S is 4,I integer ; :: thesis: for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )
then consider J being Element of S such that
A2: ( J = I & J <> the bool-sort of S & the connectives of S . 4 is_of_type {} ,J & the connectives of S . (4 + 1) is_of_type {} ,J & the connectives of S . 4 <> the connectives of S . (4 + 1) & the connectives of S . (4 + 2) is_of_type <*J*>,J & the connectives of S . (4 + 3) is_of_type <*J,J*>,J & the connectives of S . (4 + 4) is_of_type <*J,J*>,J & the connectives of S . (4 + 5) is_of_type <*J,J*>,J & the connectives of S . (4 + 3) <> the connectives of S . (4 + 4) & the connectives of S . (4 + 3) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 4) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 6) is_of_type <*J,J*>, the bool-sort of S ) ;
A3: ( len the connectives of S >= 3 & the connectives of S . 1 is_of_type {} , the bool-sort of S & the connectives of S . 2 is_of_type <* the bool-sort of S*>, the bool-sort of S & the connectives of S . 3 is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S ) by Def30;
let X be non empty set ; :: thesis: ( s in the carrier of S & s <> I & s <> the bool-sort of S implies ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A4: s in the carrier of S ; :: thesis: ( not s <> I or not s <> the bool-sort of S or ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A5: s <> I ; :: thesis: ( not s <> the bool-sort of S or ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X ) )
assume A6: s <> the bool-sort of S ; :: thesis: ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )
consider A being strict non-empty bool-correct MSAlgebra over S such that
A7: A is 4,I integer by A1, Th49;
A8: ( 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 Def31;
consider K being SortSymbol of S such that
A9: ( K = I & the connectives of S . 4 is_of_type {} ,K & the Sorts of A . K = INT & (Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) ) by A7;
set Q = the Sorts of A +* (s,X);
set F = the ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S;
set Ch = the ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S +* ( the Charact of A | ( the connectives of S .: (Seg 10)));
dom the Charact of A = the carrier' of S by PARTFUN1:def 2;
then A10: dom ( the Charact of A | ( the connectives of S .: (Seg 10))) = the connectives of S .: (Seg 10) by Th1, RELAT_1:62;
reconsider Ch = the ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S +* ( the Charact of A | ( the connectives of S .: (Seg 10))) as ManySortedFunction of the carrier' of S ;
Ch is ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S

proof

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in the carrier' of S or Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):] )
assume x in the carrier' of S ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]
then reconsider o = x as OperSymbol of S ;

per cases ( x in the connectives of S .: (Seg 10) or x nin the connectives of S .: (Seg 10) ) ;

suppose A11: x in the connectives of S .: (Seg 10) ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then A12: Ch . x = ( the Charact of A | ( the connectives of S .: (Seg 10))) . x by A10, FUNCT_4:13
.= the Charact of A . x by A11, FUNCT_1:49 ;
A13: ( (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . ( the Arity of S . o) & ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) & ((( the Sorts of A +* (s,X)) #) * the Arity of S) . o = (( the Sorts of A +* (s,X)) #) . ( the Arity of S . x) & (( the Sorts of A +* (s,X)) * the ResultSort of S) . o = ( the Sorts of A +* (s,X)) . ( the ResultSort of S . x) ) by FUNCT_2:15;
consider y being object such that
A14: ( y in dom the connectives of S & y in Seg 10 & o = the connectives of S . y ) by A11, FUNCT_1:def 6;

per cases ( 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 A14, Th23, ENUMSET1:def 8;

suppose y = 1 ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then ( the Arity of S . o = {} & the ResultSort of S . o = the bool-sort of S & <*> the carrier of S in the carrier of S * ) by A3, A14, FINSEQ_1:def 11;
then ( ( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * (<*> the carrier of S)) & (( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * (<*> the carrier of S)) & the Sorts of A . ( the ResultSort of S . o) = BOOLEAN & ( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN ) by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) by A12, A13; :: thesis: verum

end;

suppose y = 2 ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then ( the Arity of S . o = <* the bool-sort of S*> & the ResultSort of S . o = the bool-sort of S & <* the bool-sort of S*> in the carrier of S * ) by A3, A14, FINSEQ_1:def 11;
then A15: ( ( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <* the bool-sort of S*>) & (( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <* the bool-sort of S*>) & the Sorts of A . ( the ResultSort of S . o) = BOOLEAN & ( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN ) by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
( dom the Sorts of A = the carrier of S & dom ( the Sorts of A +* (s,X)) = the carrier of S ) by PARTFUN1:def 2;
then ( the Sorts of A * <* the bool-sort of S*> = <*( the Sorts of A . the bool-sort of S)*> & ( the Sorts of A +* (s,X)) * <* the bool-sort of S*> = <*(( the Sorts of A +* (s,X)) . the bool-sort of S)*> & the Sorts of A . the bool-sort of S = ( the Sorts of A +* (s,X)) . the bool-sort of S ) by A6, FUNCT_7:32, FINSEQ_2:34;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) by A12, A13, A15; :: thesis: verum

end;

suppose y = 3 ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then ( the Arity of S . o = <* the bool-sort of S, the bool-sort of S*> & the ResultSort of S . o = the bool-sort of S & <* the bool-sort of S, the bool-sort of S*> in the carrier of S * ) by A3, A14, FINSEQ_1:def 11;
then A16: ( ( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <* the bool-sort of S, the bool-sort of S*>) & (( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <* the bool-sort of S, the bool-sort of S*>) & the Sorts of A . ( the ResultSort of S . o) = BOOLEAN & ( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN ) by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
( dom the Sorts of A = the carrier of S & dom ( the Sorts of A +* (s,X)) = the carrier of S ) by PARTFUN1:def 2;
then ( the Sorts of A * <* the bool-sort of S, the bool-sort of S*> = <*( the Sorts of A . the bool-sort of S),( the Sorts of A . the bool-sort of S)*> & ( the Sorts of A +* (s,X)) * <* the bool-sort of S, the bool-sort of S*> = <*(( the Sorts of A +* (s,X)) . the bool-sort of S),(( the Sorts of A +* (s,X)) . the bool-sort of S)*> & the Sorts of A . the bool-sort of S = ( the Sorts of A +* (s,X)) . the bool-sort of S ) by A6, FUNCT_7:32, FINSEQ_2:125;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) by A12, A13, A16; :: thesis: verum

end;

suppose ( y = 4 or y = 5 ) ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then ( the Arity of S . o = {} & the ResultSort of S . o = J & <*> the carrier of S in the carrier of S * ) by A2, A14, FINSEQ_1:def 11;
then ( ( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * (<*> the carrier of S)) & (( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * (<*> the carrier of S)) & the Sorts of A . ( the ResultSort of S . o) = INT & ( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = INT ) by A5, A2, A9, FINSEQ_2:def 5, FUNCT_7:32;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) by A12, A13; :: thesis: verum

end;

suppose y = 6 ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then ( the Arity of S . o = <*J*> & the ResultSort of S . o = J & <*J*> in the carrier of S * ) by A2, A14, FINSEQ_1:def 11;
then A17: ( ( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <*J*>) & (( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <*J*>) & the Sorts of A . ( the ResultSort of S . o) = INT & ( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = INT ) by A5, A2, A9, FINSEQ_2:def 5, FUNCT_7:32;
( dom the Sorts of A = the carrier of S & dom ( the Sorts of A +* (s,X)) = the carrier of S ) by PARTFUN1:def 2;
then ( the Sorts of A * <*J*> = <*( the Sorts of A . J)*> & ( the Sorts of A +* (s,X)) * <*J*> = <*(( the Sorts of A +* (s,X)) . J)*> & the Sorts of A . J = ( the Sorts of A +* (s,X)) . J ) by A2, A5, FUNCT_7:32, FINSEQ_2:34;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) by A12, A13, A17; :: thesis: verum

end;

suppose ( y = 7 or y = 8 or y = 9 ) ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then ( the Arity of S . o = <*J,J*> & the ResultSort of S . o = J & <*J,J*> in the carrier of S * ) by A2, A14, FINSEQ_1:def 11;
then A18: ( ( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <*J,J*>) & (( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <*J,J*>) & the Sorts of A . ( the ResultSort of S . o) = INT & ( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = INT ) by A5, A2, A9, FINSEQ_2:def 5, FUNCT_7:32;
( dom the Sorts of A = the carrier of S & dom ( the Sorts of A +* (s,X)) = the carrier of S ) by PARTFUN1:def 2;
then ( the Sorts of A * <*J,J*> = <*( the Sorts of A . J),( the Sorts of A . J)*> & ( the Sorts of A +* (s,X)) * <*J,J*> = <*(( the Sorts of A +* (s,X)) . J),(( the Sorts of A +* (s,X)) . J)*> & the Sorts of A . J = ( the Sorts of A +* (s,X)) . J ) by A5, A2, FUNCT_7:32, FINSEQ_2:125;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) by A12, A13, A18; :: thesis: verum

end;

suppose y = 10 ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then ( the Arity of S . o = <*J,J*> & the ResultSort of S . o = the bool-sort of S & <*J,J*> in the carrier of S * ) by A2, A14, FINSEQ_1:def 11;
then A19: ( ( the Sorts of A #) . ( the Arity of S . o) = product ( the Sorts of A * <*J,J*>) & (( the Sorts of A +* (s,X)) #) . ( the Arity of S . o) = product (( the Sorts of A +* (s,X)) * <*J,J*>) & the Sorts of A . ( the ResultSort of S . o) = BOOLEAN & ( the Sorts of A +* (s,X)) . ( the ResultSort of S . o) = BOOLEAN ) by A6, A8, FINSEQ_2:def 5, FUNCT_7:32;
( dom the Sorts of A = the carrier of S & dom ( the Sorts of A +* (s,X)) = the carrier of S ) by PARTFUN1:def 2;
then ( the Sorts of A * <*J,J*> = <*( the Sorts of A . J),( the Sorts of A . J)*> & ( the Sorts of A +* (s,X)) * <*J,J*> = <*(( the Sorts of A +* (s,X)) . J),(( the Sorts of A +* (s,X)) . J)*> & the Sorts of A . J = ( the Sorts of A +* (s,X)) . J ) by A5, A2, FUNCT_7:32, FINSEQ_2:125;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) by A12, A13, A19; :: thesis: verum

end;

end;

end;

suppose x nin the connectives of S .: (Seg 10) ; :: thesis: Ch . x is Element of bool [:(((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x):]

then Ch . x = the ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S . x by A10, FUNCT_4:11;
hence Ch . x is Function of (((( the Sorts of A +* (s,X)) #) * the Arity of S) . x),((( the Sorts of A +* (s,X)) * the ResultSort of S) . x) ; :: thesis: verum

end;

end;

end;

then reconsider Ch = Ch as ManySortedFunction of (( the Sorts of A +* (s,X)) #) * the Arity of S,( the Sorts of A +* (s,X)) * the ResultSort of S ;
set A0 = MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #);
A20: MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) is bool-correct

proof

thus the Sorts of MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) . the bool-sort of S = the Sorts of A . the bool-sort of S by A6, FUNCT_7:32
.= BOOLEAN by Def31 ; :: according to AOFA_A00:def 31 :: thesis: ( (Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y ) ) )
4 + 6 <= len the connectives of S by A1;
then 1 <= len the connectives of S by XXREAL_0:2;
then A21: 1 in dom the connectives of S by FINSEQ_3:25;
then A22: In (( the connectives of S . 1), the carrier' of S) = the connectives of S . 1 by SUBSET_1:def 8, FUNCT_1:102;
1 in Seg 10 ;
then A23: the connectives of S . 1 in the connectives of S .: (Seg 10) by A21, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #)) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 1) by A22, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 1), the carrier' of S)),A) by A22, A23, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . {} = TRUE by Def31; :: thesis: for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y )
let x, y be boolean object ; :: thesis: ( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y )
4 + 6 <= len the connectives of S by A1;
then 2 <= len the connectives of S by XXREAL_0:2;
then A24: 2 in dom the connectives of S by FINSEQ_3:25;
then A25: In (( the connectives of S . 2), the carrier' of S) = the connectives of S . 2 by SUBSET_1:def 8, FUNCT_1:102;
2 in Seg 10 ;
then A26: In (( the connectives of S . 2), the carrier' of S) in the connectives of S .: (Seg 10) by A24, A25, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #)) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 2) by A25, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 2), the carrier' of S)),A) by A25, A26, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x*> = 'not' x by Def31; :: thesis: (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y
4 + 6 <= len the connectives of S by A1;
then 3 <= len the connectives of S by XXREAL_0:2;
then A27: 3 in dom the connectives of S by FINSEQ_3:25;
then A28: In (( the connectives of S . 3), the carrier' of S) = the connectives of S . 3 by SUBSET_1:def 8, FUNCT_1:102;
3 in Seg 10 ;
then A29: the connectives of S . 3 in the connectives of S .: (Seg 10) by A27, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #)) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 3) by A28, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 3), the carrier' of S)),A) by A28, A29, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #))) . <*x,y*> = x '&' y by Def31; :: thesis: verum

end;

MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) is non-empty ;
then reconsider A0 = MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) as non-empty bool-correct MSAlgebra over S by A20;
take A0 ; :: thesis: ( A0 is 4,I integer & the Sorts of A0 . s = X )
thus A0 is 4,I integer :: thesis: the Sorts of A0 . s = X

proof

take K ; :: according to AOFA_A00:def 49 :: thesis: ( K = I & the connectives of S . 4 is_of_type {} ,K & the Sorts of A0 . K = INT & (Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
thus ( K = I & the connectives of S . 4 is_of_type {} ,K ) by A9; :: thesis: ( the Sorts of A0 . K = INT & (Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
thus the Sorts of A0 . K = INT by A9, A5, FUNCT_7:32; :: thesis: ( (Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
4 + 6 <= len the connectives of S by A1;
then 4 <= len the connectives of S by XXREAL_0:2;
then A30: 4 in dom the connectives of S by FINSEQ_3:25;
then A31: In (( the connectives of S . 4), the carrier' of S) = the connectives of S . 4 by FUNCT_1:102, SUBSET_1:def 8;
4 in Seg 10 ;
then A32: the connectives of S . 4 in the connectives of S .: (Seg 10) by A30, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 4), the carrier' of S)),A0) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 4) by A31, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 4), the carrier' of S)),A) by A31, A32, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . 4), the carrier' of S)),A0)) . {} = 0 by A9; :: thesis: ( (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
4 + 6 <= len the connectives of S by A1;
then 5 <= len the connectives of S by XXREAL_0:2;
then A33: 5 in dom the connectives of S by FINSEQ_3:25;
then A34: In (( the connectives of S . 5), the carrier' of S) = the connectives of S . 5 by FUNCT_1:102, SUBSET_1:def 8;
5 in Seg 10 ;
then A35: the connectives of S . 5 in the connectives of S .: (Seg 10) by A33, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 5), the carrier' of S)),A0) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 5) by A34, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 5), the carrier' of S)),A) by A34, A35, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A0)) . {} = 1 by A9; :: thesis: for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
let i, j be Integer; :: thesis: ( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
4 + 6 <= len the connectives of S by A1;
then 6 <= len the connectives of S by XXREAL_0:2;
then A36: 6 in dom the connectives of S by FINSEQ_3:25;
then A37: In (( the connectives of S . 6), the carrier' of S) = the connectives of S . 6 by FUNCT_1:102, SUBSET_1:def 8;
6 in Seg 10 ;
then A38: the connectives of S . 6 in the connectives of S .: (Seg 10) by A36, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 6), the carrier' of S)),A0) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 6) by A37, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 6), the carrier' of S)),A) by A37, A38, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A0)) . <*i*> = - i by A9; :: thesis: ( (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
4 + 6 <= len the connectives of S by A1;
then 7 <= len the connectives of S by XXREAL_0:2;
then A39: 7 in dom the connectives of S by FINSEQ_3:25;
then A40: In (( the connectives of S . 7), the carrier' of S) = the connectives of S . 7 by FUNCT_1:102, SUBSET_1:def 8;
7 in Seg 10 ;
then A41: the connectives of S . 7 in the connectives of S .: (Seg 10) by A39, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 7), the carrier' of S)),A0) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 7) by A40, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 7), the carrier' of S)),A) by A40, A41, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A0)) . <*i,j*> = i + j by A9; :: thesis: ( (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )
4 + 6 <= len the connectives of S by A1;
then 8 <= len the connectives of S by XXREAL_0:2;
then A42: 8 in dom the connectives of S by FINSEQ_3:25;
then A43: In (( the connectives of S . 8), the carrier' of S) = the connectives of S . 8 by FUNCT_1:102, SUBSET_1:def 8;
8 in Seg 10 ;
then A44: the connectives of S . 8 in the connectives of S .: (Seg 10) by A42, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 8), the carrier' of S)),A0) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 8) by A43, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 8), the carrier' of S)),A) by A43, A44, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A0)) . <*i,j*> = i * j by A9; :: thesis: ( ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

hereby :: thesis: (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE)

assume A45: j <> 0 ; :: thesis: (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j
4 + 6 <= len the connectives of S by A1;
then 9 <= len the connectives of S by XXREAL_0:2;
then A46: 9 in dom the connectives of S by FINSEQ_3:25;
then A47: In (( the connectives of S . 9), the carrier' of S) = the connectives of S . 9 by FUNCT_1:102, SUBSET_1:def 8;
9 in Seg 10 ;
then A48: the connectives of S . 9 in the connectives of S .: (Seg 10) by A46, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 9), the carrier' of S)),A0) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 9) by A47, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 9), the carrier' of S)),A) by A47, A48, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A0)) . <*i,j*> = i div j by A45, A9; :: thesis: verum

end;

4 + 6 <= len the connectives of S by A1;
then A49: 10 in dom the connectives of S by FINSEQ_3:25;
then A50: In (( the connectives of S . 10), the carrier' of S) = the connectives of S . 10 by FUNCT_1:102, SUBSET_1:def 8;
10 in Seg 10 ;
then A51: the connectives of S . 10 in the connectives of S .: (Seg 10) by A49, FUNCT_1:def 6;
then Den ((In (( the connectives of S . 10), the carrier' of S)),A0) = ( the Charact of A | ( the connectives of S .: (Seg 10))) . ( the connectives of S . 10) by A50, A10, FUNCT_4:13
.= Den ((In (( the connectives of S . 10), the carrier' of S)),A) by A50, A51, FUNCT_1:49 ;
hence (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A0)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) by A9; :: thesis: verum

end;

dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
hence the Sorts of A0 . s = X by A4, FUNCT_7:31; :: thesis: verum