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

set A0 = MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #);

A20: MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) is bool-correct

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

hence the Sorts of A0 . s = X by A4, FUNCT_7:31; :: thesis: verum

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

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 ;
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 ;

end;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) )
;

end;

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;

end;.= 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;

end;

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;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

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;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

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;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

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;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

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;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

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;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

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;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

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;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

set A0 = MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #);

A20: MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) is bool-correct

proof

MSAlgebra(# ( the Sorts of A +* (s,X)),Ch #) is non-empty
;
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;.= 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

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

dom the Sorts of A = the carrier of S
by PARTFUN1:def 2;
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) )

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;( (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)

4 + 6 <= len the connectives of S
by A1;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 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

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

hence the Sorts of A0 . s = X by A4, FUNCT_7:31; :: thesis: verum