let B be non-empty MSSubAlgebra of A; :: thesis:
set n = 4;
consider I being SortSymbol of S such that
A1: ( I = 1 & the connectives of S . 4 is_of_type {} ,I & the Sorts of A . I = 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 AOFA_A00:def 50;
reconsider I = I as integer SortSymbol of S by A1, AOFA_A00:def 40;
take I ; :: according to AOFA_A00:def 49 :: thesis:
thus ( I = 1 & the connectives of S . 4 is_of_type {} ,I ) by A1; :: thesis:
the Sorts of B is MSSubset of A by MSUALG_2:def 9;
hence the Sorts of B . I c= INT by A1, PBOOLE:def 18, PBOOLE:def 2; :: according to XBOOLE_0:def 10 :: thesis:
( 4 + 6 <= len the connectives of S & 4 <= 10 ) by AOFA_A00:def 39;
then ( 4 <= len the connectives of S & 4 + 1 <= len the connectives of S & 1 <= 5 ) by XXREAL_0:2;
then ( 4 in dom the connectives of S & 4 + 1 in dom the connectives of S ) by FINSEQ_3:25;
then reconsider o1 = the connectives of S . 4, o2 = the connectives of S . (4 + 1) as OperSymbol of S by FUNCT_1:102;
( o1 is_of_type {} ,I & o2 is_of_type {} ,I ) by AOFA_A00:53;
then A2: ( Den (o1,B) is Function of (( the Sorts of B #) . {}),( the Sorts of B . I) & Den (o2,B) is Function of (( the Sorts of B #) . {}),( the Sorts of B . I) & Args (o1,B) = ( the Sorts of B #) . {} & Args (o2,B) = ( the Sorts of B #) . {} ) by Th7;
( the Sorts of B #) . (<*> the carrier of S) = {{}} by PRE_CIRC:2;
then A3: {} in ( the Sorts of B #) . {} by TARSKI:def 1;
then A4: ( (Den (o1,B)) . {} in the Sorts of B . I & (Den (o2,B)) . {} in the Sorts of B . I ) by A2, FUNCT_2:5;
A5: (Den (o1,B)) . {} = (Den (o1,A)) . {} by A2, A3, EQUATION:19
.= 0 by A1, SUBSET_1:def 8 ;
A6: (Den (o2,B)) . {} = (Den (o2,A)) . {} by A2, A3, EQUATION:19
.= 1 by A1, SUBSET_1:def 8 ;
defpred S₁[ Nat] means ( S in the Sorts of B . I & - S in the Sorts of B . I );
A7: S₁[ 0 ] by A2, A3, A5, FUNCT_2:5;
( 4 + 6 <= len the connectives of S & 4 <= 10 ) by AOFA_A00:def 39;
then ( 4 + 2 <= len the connectives of S & 4 + 3 <= len the connectives of S & 1 <= 6 & 1 <= 7 ) by XXREAL_0:2;
then ( 4 + 2 in dom the connectives of S & 4 + 3 in dom the connectives of S ) by FINSEQ_3:25;
then reconsider o3 = the connectives of S . (4 + 2), o4 = the connectives of S . (4 + 3) as OperSymbol of S by FUNCT_1:102;
( o3 is_of_type <*I*>,I & o4 is_of_type <*I,I*>,I ) by AOFA_A00:53;
then A8: ( Den (o3,B) is Function of (( the Sorts of B #) . <*I*>),( the Sorts of B . I) & Den (o4,B) is Function of (( the Sorts of B #) . <*I,I*>),( the Sorts of B . I) & Args (o3,B) = ( the Sorts of B #) . <*I*> & Args (o4,B) = ( the Sorts of B #) . <*I,I*> ) by Th7;
A9: dom the Sorts of B = the carrier of S by PARTFUN1:def 2;
<*I*> is Element of the carrier of S * by FINSEQ_1:def 11;
then A10: Args (o3,B) = product ( the Sorts of B * <*I*>) by A8, FINSEQ_2:def 5
.= product <*( the Sorts of B . I)*> by A9, FINSEQ_2:34 ;
<*I,I*> is Element of the carrier of S * by FINSEQ_1:def 11;
then A11: Args (o4,B) = product ( the Sorts of B * <*I,I*>) by A8, FINSEQ_2:def 5
.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A9, FINSEQ_2:125 ;
A12: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A13: S₁[i] ; :: thesis:
then A14: <*i,1*> in Args (o4,B) by A6, A4, A11, FINSEQ_3:124;
(Den (o4,B)) . <*i,1*> = (Den (o4,A)) . <*i,1*> by A13, A6, A4, A11, FINSEQ_3:124, EQUATION:19
.= (Den ((In (o4, the carrier' of S)),A)) . <*i,1*> by SUBSET_1:def 8
.= i + 1 by A1 ;
hence A15: i + 1 in the Sorts of B . I by A14, A8, FUNCT_2:5; :: thesis:
then A16: <*(i + 1)*> in Args (o3,B) by A10, FINSEQ_3:123;
(Den (o3,B)) . <*(i + 1)*> = (Den (o3,A)) . <*(i + 1)*> by A15, A10, FINSEQ_3:123, EQUATION:19
.= (Den ((In (o3, the carrier' of S)),A)) . <*(i + 1)*> by SUBSET_1:def 8
.= - (i + 1) by A1 ;
hence - (i + 1) in the Sorts of B . I by A16, A8, FUNCT_2:5; :: thesis:

end;

A17: for i being Nat holds S₁[i] from NAT_1:sch 2(A7, A12);
thus A18: INT c= the Sorts of B . I :: thesis:

proof

let x be Integer; :: according to MEMBERED:def 11 :: thesis:
x in INT by INT_1:def 2;
then consider n being Nat such that
A19: ( x = n or x = - n ) by INT_1:def 1;
thus ( not x in INT or x in the Sorts of B . I ) by A17, A19; :: thesis:

end;

thus ( (Den ((In (( the connectives of S . 4), the carrier' of S)),B)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),B)) . {} = 1 ) by A5, A6, SUBSET_1:def 8; :: thesis:
let i, j be Integer; :: thesis:
A20: ( i in INT & j in INT ) by INT_1:def 2;
<*i*> in Args (o3,B) by A20, A18, A10, FINSEQ_3:123;
then <*i*> in Args ((In (o3, the carrier' of S)),B) by SUBSET_1:def 8;
hence (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),B)) . <*i*> = (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A)) . <*i*> by EQUATION:19
.= - i by A1 ;
:: thesis:
<*i,j*> in Args (o4,B) by A11, A20, A18, FINSEQ_3:124;
then <*i,j*> in Args ((In (o4, the carrier' of S)),B) by SUBSET_1:def 8;
hence (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),B)) . <*i,j*> = (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A)) . <*i,j*> by EQUATION:19
.= i + j by A1 ;
:: thesis:
( 4 + 6 <= len the connectives of S & 4 <= 10 ) by AOFA_A00:def 39;
then ( 4 + 4 <= len the connectives of S & 4 + 5 <= len the connectives of S & 1 <= 8 & 1 <= 9 ) by XXREAL_0:2;
then ( 4 + 4 in dom the connectives of S & 4 + 5 in dom the connectives of S ) by FINSEQ_3:25;
then reconsider o5 = the connectives of S . (4 + 4), o6 = the connectives of S . (4 + 5) as OperSymbol of S by FUNCT_1:102;
( o5 is_of_type <*I,I*>,I & o6 is_of_type <*I,I*>,I ) by AOFA_A00:53;
then A21: ( Args (o5,B) = ( the Sorts of B #) . <*I,I*> & Args (o6,B) = ( the Sorts of B #) . <*I,I*> ) by Th7;
then <*i,j*> in Args (o5,B) by A8, A11, A20, A18, FINSEQ_3:124;
then <*i,j*> in Args ((In (o5, the carrier' of S)),B) by SUBSET_1:def 8;
hence (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),B)) . <*i,j*> = (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A)) . <*i,j*> by EQUATION:19
.= i * j by A1 ;
:: thesis:

hereby :: thesis:

assume A22: j <> 0 ; :: thesis:
<*i,j*> in Args (o6,B) by A8, A11, A20, A18, A21, FINSEQ_3:124;
then <*i,j*> in Args ((In (o6, the carrier' of S)),B) by SUBSET_1:def 8;
hence (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),B)) . <*i,j*> = (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A)) . <*i,j*> by EQUATION:19
.= i div j by A22, A1 ;
:: thesis:

end;

( 4 + 6 <= len the connectives of S & 4 <= 10 ) by AOFA_A00:def 39;
then 4 + 6 in dom the connectives of S by FINSEQ_3:25;
then reconsider o7 = the connectives of S . (4 + 6) as OperSymbol of S by FUNCT_1:102;
o7 is_of_type <*I,I*>, the bool-sort of S by AOFA_A00:53;
then Args (o7,B) = ( the Sorts of B #) . <*I,I*> by Th7;
then <*i,j*> in Args (o7,B) by A8, A11, A20, A18, FINSEQ_3:124;
then <*i,j*> in Args ((In (o7, the carrier' of S)),B) by SUBSET_1:def 8;
hence (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),B)) . <*i,j*> = (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A)) . <*i,j*> by EQUATION:19
.= IFGT (i,j,FALSE,TRUE) by A1 ;
:: thesis: