let n be Nat; :: thesis: for I being set st n >= 1 holds

for S being non empty non void bool-correct BoolSignature st S is n,I integer holds

ex A being strict non-empty bool-correct MSAlgebra over S st A is n,I integer

let J be set ; :: thesis: ( n >= 1 implies for S being non empty non void bool-correct BoolSignature st S is n,J integer holds

ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer )

assume A1: n >= 1 ; :: thesis: for S being non empty non void bool-correct BoolSignature st S is n,J integer holds

ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer

let S be non empty non void bool-correct BoolSignature ; :: thesis: ( S is n,J integer implies ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer )

assume A2: S is n,J integer ; :: thesis: ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer

then consider I being Element of S such that

A3: ( I = J & I <> the bool-sort of S & the connectives of S . n is_of_type {} ,I & the connectives of S . (n + 1) is_of_type {} ,I & the connectives of S . n <> the connectives of S . (n + 1) & the connectives of S . (n + 2) is_of_type <*I*>,I & the connectives of S . (n + 3) is_of_type <*I,I*>,I & the connectives of S . (n + 4) is_of_type <*I,I*>,I & the connectives of S . (n + 5) is_of_type <*I,I*>,I & the connectives of S . (n + 3) <> the connectives of S . (n + 4) & the connectives of S . (n + 3) <> the connectives of S . (n + 5) & the connectives of S . (n + 4) <> the connectives of S . (n + 5) & the connectives of S . (n + 6) is_of_type <*I,I*>, the bool-sort of S ) ;

set X = the V2() ManySortedSet of the carrier of S;

set A = the V2() ManySortedSet of the carrier of S +* (I,INT);

consider B being strict non-empty MSAlgebra over S such that

A4: ( the Sorts of B = ( the V2() ManySortedSet of the carrier of S +* (I,INT)) +* ( the bool-sort of S,BOOLEAN) & B is bool-correct ) by Th46;

set C = the Sorts of B;

set Ch = the Charact of B;

set bs = the bool-sort of S;

A5: len the connectives of S >= n + 6 by A2;

( n + 4 <= (n + 4) + 2 & n + 3 <= (n + 3) + 3 & n + 2 <= (n + 2) + 4 & n + 1 <= (n + 1) + 5 & n <= n + 6 & 1 <= 1 + (n + 5) & 2 <= 2 + (n + 4) & 3 <= 3 + (n + 3) & 1 <= 1 + (n + 3) & 1 <= 1 + (n + 2) & n + 5 <= (n + 5) + 1 & 1 <= 1 + (n + 1) & 1 <= n + 1 ) by NAT_1:12;

then ( n + 5 <= len the connectives of S & n + 4 <= len the connectives of S & n + 3 <= len the connectives of S & n + 2 <= len the connectives of S & n + 1 <= len the connectives of S & 3 <= len the connectives of S & 1 <= len the connectives of S & 2 <= len the connectives of S & n <= len the connectives of S ) by A5, XXREAL_0:2;

then ( 1 in dom the connectives of S & 2 in dom the connectives of S & 3 in dom the connectives of S & n in dom the connectives of S & n + 1 in dom the connectives of S & n + 2 in dom the connectives of S & n + 3 in dom the connectives of S & n + 4 in dom the connectives of S & n + 5 in dom the connectives of S & n + 6 in dom the connectives of S ) by A5, A1, FINSEQ_3:25, NAT_1:12;

then reconsider o01 = the connectives of S . 1, o02 = the connectives of S . 2, o03 = the connectives of S . 3, o1 = the connectives of S . n, o2 = the connectives of S . (n + 1), o3 = the connectives of S . (n + 2), o4 = the connectives of S . (n + 3), o5 = the connectives of S . (n + 4), o6 = the connectives of S . (n + 5), o7 = the connectives of S . (n + 6) as OperSymbol of S by DTCONSTR:2;

set g0 = (0 -tuples_on INT) --> 0;

set g1 = (0 -tuples_on INT) --> 1;

A6: ( dom ((0 -tuples_on INT) --> 0) = 0 -tuples_on INT & dom ((0 -tuples_on INT) --> 1) = 0 -tuples_on INT ) ;

( {0} c= INT & {1} c= INT ) by INT_1:def 2;

then ( rng ((0 -tuples_on INT) --> 0) c= INT & rng ((0 -tuples_on INT) --> 1) c= INT ) ;

then reconsider g0 = (0 -tuples_on INT) --> 0, g1 = (0 -tuples_on INT) --> 1 as Function of (0 -tuples_on INT),INT by A6, FUNCT_2:2;

deffunc H_{1}( Element of INT ) -> Element of INT = In ((- $1),INT);

consider f1 being non empty homogeneous quasi_total 1 -ary PartFunc of (INT *),INT such that

A7: for a being Element of INT holds f1 . <*a*> = H_{1}(a)
from AOFA_A00:sch 2();

A8: dom f1 = (arity f1) -tuples_on INT by COMPUT_1:22

.= 1 -tuples_on INT by COMPUT_1:def 21 ;

A9: rng f1 c= INT by RELAT_1:def 19;

A10: <*I*> in the carrier of S * by FINSEQ_1:def 11;

A11: ( dom ( the V2() ManySortedSet of the carrier of S +* (I,INT)) = the carrier of S & dom the V2() ManySortedSet of the carrier of S = the carrier of S & dom the Sorts of B = the carrier of S ) by PARTFUN1:def 2;

A12: the Sorts of B . I = ( the V2() ManySortedSet of the carrier of S +* (I,INT)) . I by A4, A3, FUNCT_7:32

.= INT by A11, FUNCT_7:31 ;

A13: ( the_arity_of o3 = <*I*> & the_result_sort_of o3 = I ) by A3;

then A14: (( the Sorts of B #) * the Arity of S) . o3 = ( the Sorts of B #) . <*I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I*>) by A10, FINSEQ_2:def 5

.= product <*( the Sorts of B . I)*> by A11, FINSEQ_2:34

.= 1 -tuples_on INT by A12, FINSEQ_3:126 ;

( the Sorts of B * the ResultSort of S) . o3 = the Sorts of B . I by A13, FUNCT_2:15;

then f1 is Function of ((( the Sorts of B #) * the Arity of S) . o3),(( the Sorts of B * the ResultSort of S) . o3) by A14, A12, A8, A9, FUNCT_2:2;

then reconsider Ch1 = the Charact of B +* (o3,f1) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H_{2}( Element of INT , Element of INT ) -> Element of INT = In (($1 + $2),INT);

consider f2 being non empty homogeneous quasi_total 2 -ary PartFunc of (INT *),INT such that

A15: for a, b being Element of INT holds f2 . <*a,b*> = H_{2}(a,b)
from AOFA_A00:sch 3();

A16: dom f2 = (arity f2) -tuples_on INT by COMPUT_1:22

.= 2 -tuples_on INT by COMPUT_1:def 21 ;

A17: rng f2 c= INT by RELAT_1:def 19;

A18: <*I,I*> in the carrier of S * by FINSEQ_1:def 11;

A19: ( the_arity_of o4 = <*I,I*> & the_result_sort_of o4 = I ) by A3;

then A20: (( the Sorts of B #) * the Arity of S) . o4 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o4 = the Sorts of B . I by A19, FUNCT_2:15;

then f2 is Function of ((( the Sorts of B #) * the Arity of S) . o4),(( the Sorts of B * the ResultSort of S) . o4) by A20, A12, A16, A17, FUNCT_2:2;

then reconsider Ch2 = Ch1 +* (o4,f2) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H_{3}( Element of INT , Element of INT ) -> Element of INT = In (($1 * $2),INT);

consider f3 being non empty homogeneous quasi_total 2 -ary PartFunc of (INT *),INT such that

A21: for a, b being Element of INT holds f3 . <*a,b*> = H_{3}(a,b)
from AOFA_A00:sch 3();

A22: dom f3 = (arity f3) -tuples_on INT by COMPUT_1:22

.= 2 -tuples_on INT by COMPUT_1:def 21 ;

A23: rng f3 c= INT by RELAT_1:def 19;

A24: ( the_arity_of o5 = <*I,I*> & the_result_sort_of o5 = I ) by A3;

then A25: (( the Sorts of B #) * the Arity of S) . o5 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o5 = the Sorts of B . I by A24, FUNCT_2:15;

then f3 is Function of ((( the Sorts of B #) * the Arity of S) . o5),(( the Sorts of B * the ResultSort of S) . o5) by A25, A12, A22, A23, FUNCT_2:2;

then reconsider Ch3 = Ch2 +* (o5,f3) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H_{4}( Element of INT , Element of INT ) -> Element of INT = In (($1 div $2),INT);

consider fa being non empty homogeneous quasi_total 2 -ary PartFunc of (INT *),INT such that

A26: for a, b being Element of INT holds fa . <*a,b*> = H_{4}(a,b)
from AOFA_A00:sch 3();

A27: dom fa = (arity fa) -tuples_on INT by COMPUT_1:22

.= 2 -tuples_on INT by COMPUT_1:def 21 ;

A28: rng fa c= INT by RELAT_1:def 19;

A29: ( the_arity_of o6 = <*I,I*> & the_result_sort_of o6 = I ) by A3;

then A30: (( the Sorts of B #) * the Arity of S) . o6 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o6 = the Sorts of B . I by A29, FUNCT_2:15;

then fa is Function of ((( the Sorts of B #) * the Arity of S) . o6),(( the Sorts of B * the ResultSort of S) . o6) by A30, A12, A27, A28, FUNCT_2:2;

then reconsider Ch3a = Ch3 +* (o6,fa) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H_{5}( Element of 2 -tuples_on INT) -> Element of BOOLEAN = In ((IFGT (($1 /. 1),($1 /. 2),FALSE,TRUE)),BOOLEAN);

consider f4 being Function of (2 -tuples_on INT),BOOLEAN such that

A31: for p being Element of 2 -tuples_on INT holds f4 . p = H_{5}(p)
from FUNCT_2:sch 4();

A32: ( the_arity_of o7 = <*I,I*> & the_result_sort_of o7 = the bool-sort of S ) by A3;

then A33: (( the Sorts of B #) * the Arity of S) . o7 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o7 = the Sorts of B . the bool-sort of S by A32, FUNCT_2:15

.= BOOLEAN by A4 ;

then reconsider Ch4 = Ch3a +* (o7,f4) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by A33, Th45;

A34: <*> the carrier of S in the carrier of S * by FINSEQ_1:def 11;

A35: ( the_arity_of o1 = {} & the_result_sort_of o1 = I ) by A3;

then A36: (( the Sorts of B #) * the Arity of S) . o1 = ( the Sorts of B #) . {} by FUNCT_2:15

.= product ( the Sorts of B * (<*> INT)) by A34, FINSEQ_2:def 5

.= 0 -tuples_on INT by CARD_3:10, FINSEQ_2:94 ;

( the Sorts of B * the ResultSort of S) . o1 = INT by A12, A35, FUNCT_2:15;

then reconsider Ch5 = Ch4 +* (o1,g0) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by A36, Th45;

A37: ( the_arity_of o2 = {} & the_result_sort_of o2 = I ) by A3;

then A38: (( the Sorts of B #) * the Arity of S) . o2 = ( the Sorts of B #) . {} by FUNCT_2:15

.= product ( the Sorts of B * (<*> INT)) by A34, FINSEQ_2:def 5

.= 0 -tuples_on INT by CARD_3:10, FINSEQ_2:94 ;

( the Sorts of B * the ResultSort of S) . o2 = INT by A12, A37, FUNCT_2:15;

then reconsider Ch6 = Ch5 +* (o2,g1) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by A38, Th45;

A39: ( dom Ch5 = the carrier' of S & dom Ch4 = the carrier' of S & dom Ch3 = the carrier' of S & dom Ch2 = the carrier' of S & dom Ch1 = the carrier' of S & dom the Charact of B = the carrier' of S & dom Ch3a = the carrier' of S ) by PARTFUN1:def 2;

set D = MSAlgebra(# the Sorts of B,Ch6 #);

( MSAlgebra(# the Sorts of B,Ch6 #) is non-empty & MSAlgebra(# the Sorts of B,Ch6 #) is bool-correct )

take D ; :: thesis: D is n,J integer

take I ; :: according to AOFA_A00:def 49 :: thesis: ( I = J & the connectives of S . n is_of_type {} ,I & the Sorts of D . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

thus I = J by A3; :: thesis: ( the connectives of S . n is_of_type {} ,I & the Sorts of D . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

thus the connectives of S . n is_of_type {} ,I by A3; :: thesis: ( the Sorts of D . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

thus the Sorts of D . I = ( the V2() ManySortedSet of the carrier of S +* (I,INT)) . I by A3, A4, FUNCT_7:32

.= INT by A11, FUNCT_7:31 ; :: thesis: ( (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

A46: ( {} in {{}} & 0 -tuples_on INT = {(<*> INT)} ) by TARSKI:def 1, FINSEQ_2:94;

Ch6 . o1 = Ch5 . o1 by A3, FUNCT_7:32

.= g0 by A39, FUNCT_7:31 ;

hence (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 ; :: thesis: ( (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

Ch6 . o2 = g1 by A39, FUNCT_7:31;

hence (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 by A46, FUNCOP_1:7; :: thesis: for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

let i, j be Integer; :: thesis: ( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

( len <*I*> = 1 & len <*I,I*> = 2 ) by FINSEQ_1:40, FINSEQ_1:44;

then A48: ( o3 <> o4 & o3 <> o5 & o3 <> o6 & o3 <> o1 & o3 <> o2 & o3 <> o7 ) by A3;

A49: Ch6 . o3 = Ch5 . o3 by A13, A37, FUNCT_7:32

.= Ch4 . o3 by A13, A35, FUNCT_7:32

.= Ch3a . o3 by A48, FUNCT_7:32

.= Ch3 . o3 by A48, FUNCT_7:32

.= Ch2 . o3 by A48, FUNCT_7:32

.= Ch1 . o3 by A48, FUNCT_7:32

.= f1 by A39, FUNCT_7:31 ;

( In (o3, the carrier' of S) = o3 & i in INT & - i in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = In ((- i),INT) by A7, A49

.= - i ;

:: thesis: ( (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

A50: Ch6 . o4 = Ch5 . o4 by A19, A37, FUNCT_7:32

.= Ch4 . o4 by A19, A35, FUNCT_7:32

.= Ch3a . o4 by A3, FUNCT_7:32

.= Ch3 . o4 by A3, FUNCT_7:32

.= Ch2 . o4 by A3, FUNCT_7:32

.= f2 by A39, FUNCT_7:31 ;

( In (o4, the carrier' of S) = o4 & i in INT & j in INT & i + j in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = In ((i + j),INT) by A15, A50

.= i + j ;

:: thesis: ( (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

A51: ( o5 <> o6 & o5 <> o1 & o5 <> o2 & o5 <> o7 ) by A3;

A52: Ch6 . o5 = Ch5 . o5 by A51, FUNCT_7:32

.= Ch4 . o5 by A51, FUNCT_7:32

.= Ch3a . o5 by A51, FUNCT_7:32

.= Ch3 . o5 by A3, FUNCT_7:32

.= f3 by A39, FUNCT_7:31 ;

A53: ( In (o5, the carrier' of S) = o5 & i in INT & j in INT & i * j in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = In ((i * j),INT) by A21, A52

.= i * j ;

:: thesis: ( ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

.= Ch4 . o7 by A32, A35, FUNCT_7:32

.= f4 by A39, FUNCT_7:31 ;

reconsider p = <*i,j*> as Element of 2 -tuples_on INT by A53, FINSEQ_2:101;

dom <*i,j*> = Seg 2 by FINSEQ_1:89;

then ( 1 in dom <*i,j*> & 2 in dom <*i,j*> ) ;

then A57: ( p /. 1 = p . 1 & p /. 2 = p . 2 & p . 1 = i & p . 2 = j ) by FINSEQ_1:44, PARTFUN1:def 6;

A58: ( In (o7, the carrier' of S) = o7 & i in INT & j in INT & ( i > j implies IFGT (i,j,FALSE,TRUE) = FALSE ) & ( i <= j implies IFGT (i,j,FALSE,TRUE) = TRUE ) & FALSE in BOOLEAN & TRUE in BOOLEAN ) by INT_1:def 2, XXREAL_0:def 11;

thus (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = H_{5}(p)
by A56, A31

.= IFGT (i,j,FALSE,TRUE) by A58, A57 ; :: thesis: verum

for S being non empty non void bool-correct BoolSignature st S is n,I integer holds

ex A being strict non-empty bool-correct MSAlgebra over S st A is n,I integer

let J be set ; :: thesis: ( n >= 1 implies for S being non empty non void bool-correct BoolSignature st S is n,J integer holds

ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer )

assume A1: n >= 1 ; :: thesis: for S being non empty non void bool-correct BoolSignature st S is n,J integer holds

ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer

let S be non empty non void bool-correct BoolSignature ; :: thesis: ( S is n,J integer implies ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer )

assume A2: S is n,J integer ; :: thesis: ex A being strict non-empty bool-correct MSAlgebra over S st A is n,J integer

then consider I being Element of S such that

A3: ( I = J & I <> the bool-sort of S & the connectives of S . n is_of_type {} ,I & the connectives of S . (n + 1) is_of_type {} ,I & the connectives of S . n <> the connectives of S . (n + 1) & the connectives of S . (n + 2) is_of_type <*I*>,I & the connectives of S . (n + 3) is_of_type <*I,I*>,I & the connectives of S . (n + 4) is_of_type <*I,I*>,I & the connectives of S . (n + 5) is_of_type <*I,I*>,I & the connectives of S . (n + 3) <> the connectives of S . (n + 4) & the connectives of S . (n + 3) <> the connectives of S . (n + 5) & the connectives of S . (n + 4) <> the connectives of S . (n + 5) & the connectives of S . (n + 6) is_of_type <*I,I*>, the bool-sort of S ) ;

set X = the V2() ManySortedSet of the carrier of S;

set A = the V2() ManySortedSet of the carrier of S +* (I,INT);

consider B being strict non-empty MSAlgebra over S such that

A4: ( the Sorts of B = ( the V2() ManySortedSet of the carrier of S +* (I,INT)) +* ( the bool-sort of S,BOOLEAN) & B is bool-correct ) by Th46;

set C = the Sorts of B;

set Ch = the Charact of B;

set bs = the bool-sort of S;

A5: len the connectives of S >= n + 6 by A2;

( n + 4 <= (n + 4) + 2 & n + 3 <= (n + 3) + 3 & n + 2 <= (n + 2) + 4 & n + 1 <= (n + 1) + 5 & n <= n + 6 & 1 <= 1 + (n + 5) & 2 <= 2 + (n + 4) & 3 <= 3 + (n + 3) & 1 <= 1 + (n + 3) & 1 <= 1 + (n + 2) & n + 5 <= (n + 5) + 1 & 1 <= 1 + (n + 1) & 1 <= n + 1 ) by NAT_1:12;

then ( n + 5 <= len the connectives of S & n + 4 <= len the connectives of S & n + 3 <= len the connectives of S & n + 2 <= len the connectives of S & n + 1 <= len the connectives of S & 3 <= len the connectives of S & 1 <= len the connectives of S & 2 <= len the connectives of S & n <= len the connectives of S ) by A5, XXREAL_0:2;

then ( 1 in dom the connectives of S & 2 in dom the connectives of S & 3 in dom the connectives of S & n in dom the connectives of S & n + 1 in dom the connectives of S & n + 2 in dom the connectives of S & n + 3 in dom the connectives of S & n + 4 in dom the connectives of S & n + 5 in dom the connectives of S & n + 6 in dom the connectives of S ) by A5, A1, FINSEQ_3:25, NAT_1:12;

then reconsider o01 = the connectives of S . 1, o02 = the connectives of S . 2, o03 = the connectives of S . 3, o1 = the connectives of S . n, o2 = the connectives of S . (n + 1), o3 = the connectives of S . (n + 2), o4 = the connectives of S . (n + 3), o5 = the connectives of S . (n + 4), o6 = the connectives of S . (n + 5), o7 = the connectives of S . (n + 6) as OperSymbol of S by DTCONSTR:2;

set g0 = (0 -tuples_on INT) --> 0;

set g1 = (0 -tuples_on INT) --> 1;

A6: ( dom ((0 -tuples_on INT) --> 0) = 0 -tuples_on INT & dom ((0 -tuples_on INT) --> 1) = 0 -tuples_on INT ) ;

( {0} c= INT & {1} c= INT ) by INT_1:def 2;

then ( rng ((0 -tuples_on INT) --> 0) c= INT & rng ((0 -tuples_on INT) --> 1) c= INT ) ;

then reconsider g0 = (0 -tuples_on INT) --> 0, g1 = (0 -tuples_on INT) --> 1 as Function of (0 -tuples_on INT),INT by A6, FUNCT_2:2;

deffunc H

consider f1 being non empty homogeneous quasi_total 1 -ary PartFunc of (INT *),INT such that

A7: for a being Element of INT holds f1 . <*a*> = H

A8: dom f1 = (arity f1) -tuples_on INT by COMPUT_1:22

.= 1 -tuples_on INT by COMPUT_1:def 21 ;

A9: rng f1 c= INT by RELAT_1:def 19;

A10: <*I*> in the carrier of S * by FINSEQ_1:def 11;

A11: ( dom ( the V2() ManySortedSet of the carrier of S +* (I,INT)) = the carrier of S & dom the V2() ManySortedSet of the carrier of S = the carrier of S & dom the Sorts of B = the carrier of S ) by PARTFUN1:def 2;

A12: the Sorts of B . I = ( the V2() ManySortedSet of the carrier of S +* (I,INT)) . I by A4, A3, FUNCT_7:32

.= INT by A11, FUNCT_7:31 ;

A13: ( the_arity_of o3 = <*I*> & the_result_sort_of o3 = I ) by A3;

then A14: (( the Sorts of B #) * the Arity of S) . o3 = ( the Sorts of B #) . <*I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I*>) by A10, FINSEQ_2:def 5

.= product <*( the Sorts of B . I)*> by A11, FINSEQ_2:34

.= 1 -tuples_on INT by A12, FINSEQ_3:126 ;

( the Sorts of B * the ResultSort of S) . o3 = the Sorts of B . I by A13, FUNCT_2:15;

then f1 is Function of ((( the Sorts of B #) * the Arity of S) . o3),(( the Sorts of B * the ResultSort of S) . o3) by A14, A12, A8, A9, FUNCT_2:2;

then reconsider Ch1 = the Charact of B +* (o3,f1) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H

consider f2 being non empty homogeneous quasi_total 2 -ary PartFunc of (INT *),INT such that

A15: for a, b being Element of INT holds f2 . <*a,b*> = H

A16: dom f2 = (arity f2) -tuples_on INT by COMPUT_1:22

.= 2 -tuples_on INT by COMPUT_1:def 21 ;

A17: rng f2 c= INT by RELAT_1:def 19;

A18: <*I,I*> in the carrier of S * by FINSEQ_1:def 11;

A19: ( the_arity_of o4 = <*I,I*> & the_result_sort_of o4 = I ) by A3;

then A20: (( the Sorts of B #) * the Arity of S) . o4 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o4 = the Sorts of B . I by A19, FUNCT_2:15;

then f2 is Function of ((( the Sorts of B #) * the Arity of S) . o4),(( the Sorts of B * the ResultSort of S) . o4) by A20, A12, A16, A17, FUNCT_2:2;

then reconsider Ch2 = Ch1 +* (o4,f2) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H

consider f3 being non empty homogeneous quasi_total 2 -ary PartFunc of (INT *),INT such that

A21: for a, b being Element of INT holds f3 . <*a,b*> = H

A22: dom f3 = (arity f3) -tuples_on INT by COMPUT_1:22

.= 2 -tuples_on INT by COMPUT_1:def 21 ;

A23: rng f3 c= INT by RELAT_1:def 19;

A24: ( the_arity_of o5 = <*I,I*> & the_result_sort_of o5 = I ) by A3;

then A25: (( the Sorts of B #) * the Arity of S) . o5 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o5 = the Sorts of B . I by A24, FUNCT_2:15;

then f3 is Function of ((( the Sorts of B #) * the Arity of S) . o5),(( the Sorts of B * the ResultSort of S) . o5) by A25, A12, A22, A23, FUNCT_2:2;

then reconsider Ch3 = Ch2 +* (o5,f3) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H

consider fa being non empty homogeneous quasi_total 2 -ary PartFunc of (INT *),INT such that

A26: for a, b being Element of INT holds fa . <*a,b*> = H

A27: dom fa = (arity fa) -tuples_on INT by COMPUT_1:22

.= 2 -tuples_on INT by COMPUT_1:def 21 ;

A28: rng fa c= INT by RELAT_1:def 19;

A29: ( the_arity_of o6 = <*I,I*> & the_result_sort_of o6 = I ) by A3;

then A30: (( the Sorts of B #) * the Arity of S) . o6 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o6 = the Sorts of B . I by A29, FUNCT_2:15;

then fa is Function of ((( the Sorts of B #) * the Arity of S) . o6),(( the Sorts of B * the ResultSort of S) . o6) by A30, A12, A27, A28, FUNCT_2:2;

then reconsider Ch3a = Ch3 +* (o6,fa) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by Th45;

deffunc H

consider f4 being Function of (2 -tuples_on INT),BOOLEAN such that

A31: for p being Element of 2 -tuples_on INT holds f4 . p = H

A32: ( the_arity_of o7 = <*I,I*> & the_result_sort_of o7 = the bool-sort of S ) by A3;

then A33: (( the Sorts of B #) * the Arity of S) . o7 = ( the Sorts of B #) . <*I,I*> by FUNCT_2:15

.= product ( the Sorts of B * <*I,I*>) by A18, FINSEQ_2:def 5

.= product <*( the Sorts of B . I),( the Sorts of B . I)*> by A11, FINSEQ_2:125

.= 2 -tuples_on INT by A12, FINSEQ_3:128 ;

( the Sorts of B * the ResultSort of S) . o7 = the Sorts of B . the bool-sort of S by A32, FUNCT_2:15

.= BOOLEAN by A4 ;

then reconsider Ch4 = Ch3a +* (o7,f4) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by A33, Th45;

A34: <*> the carrier of S in the carrier of S * by FINSEQ_1:def 11;

A35: ( the_arity_of o1 = {} & the_result_sort_of o1 = I ) by A3;

then A36: (( the Sorts of B #) * the Arity of S) . o1 = ( the Sorts of B #) . {} by FUNCT_2:15

.= product ( the Sorts of B * (<*> INT)) by A34, FINSEQ_2:def 5

.= 0 -tuples_on INT by CARD_3:10, FINSEQ_2:94 ;

( the Sorts of B * the ResultSort of S) . o1 = INT by A12, A35, FUNCT_2:15;

then reconsider Ch5 = Ch4 +* (o1,g0) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by A36, Th45;

A37: ( the_arity_of o2 = {} & the_result_sort_of o2 = I ) by A3;

then A38: (( the Sorts of B #) * the Arity of S) . o2 = ( the Sorts of B #) . {} by FUNCT_2:15

.= product ( the Sorts of B * (<*> INT)) by A34, FINSEQ_2:def 5

.= 0 -tuples_on INT by CARD_3:10, FINSEQ_2:94 ;

( the Sorts of B * the ResultSort of S) . o2 = INT by A12, A37, FUNCT_2:15;

then reconsider Ch6 = Ch5 +* (o2,g1) as ManySortedFunction of ( the Sorts of B #) * the Arity of S, the Sorts of B * the ResultSort of S by A38, Th45;

A39: ( dom Ch5 = the carrier' of S & dom Ch4 = the carrier' of S & dom Ch3 = the carrier' of S & dom Ch2 = the carrier' of S & dom Ch1 = the carrier' of S & dom the Charact of B = the carrier' of S & dom Ch3a = the carrier' of S ) by PARTFUN1:def 2;

set D = MSAlgebra(# the Sorts of B,Ch6 #);

( MSAlgebra(# the Sorts of B,Ch6 #) is non-empty & MSAlgebra(# the Sorts of B,Ch6 #) is bool-correct )

proof

then reconsider D = MSAlgebra(# the Sorts of B,Ch6 #) as strict non-empty bool-correct MSAlgebra over S ;
thus
the Sorts of MSAlgebra(# the Sorts of B,Ch6 #) is V2()
; :: according to MSUALG_1:def 3 :: thesis: MSAlgebra(# the Sorts of B,Ch6 #) is bool-correct

thus the Sorts of MSAlgebra(# the Sorts of B,Ch6 #) . the bool-sort of S = BOOLEAN by A4; :: according to AOFA_A00:def 31 :: thesis: ( (Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . {} = TRUE & ( for x, y being boolean object holds

( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = x '&' y ) ) )

( o01 is_of_type {} , the bool-sort of S & o02 is_of_type <* the bool-sort of S*>, the bool-sort of S & o03 is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S ) by Def30;

then ( the_arity_of o01 = {} & the_result_sort_of o01 = the bool-sort of S & the_result_sort_of o02 = the bool-sort of S & the_result_sort_of o03 = the bool-sort of S & the_arity_of o02 = <* the bool-sort of S*> & the_arity_of o03 = <* the bool-sort of S, the bool-sort of S*> & len <* the bool-sort of S*> = 1 & len <*I,I*> = 2 & <*I,I*> . 1 = I & <* the bool-sort of S, the bool-sort of S*> . 1 = the bool-sort of S ) by FINSEQ_1:40, FINSEQ_1:44;

then A40: ( o01 <> o4 & o01 <> o3 & o01 <> o2 & o01 <> o1 & o01 <> o5 & o01 <> o6 & o02 <> o4 & o02 <> o3 & o02 <> o2 & o02 <> o1 & o02 <> o5 & o02 <> o6 & o03 <> o4 & o03 <> o3 & o03 <> o2 & o03 <> o1 & o03 <> o5 & o03 <> o6 & o01 <> o7 & o02 <> o7 & o03 <> o7 ) by A3;

A41: Ch6 . o01 = Ch5 . o01 by A40, FUNCT_7:32

.= Ch4 . o01 by A40, FUNCT_7:32

.= Ch3a . o01 by A40, FUNCT_7:32

.= Ch3 . o01 by A40, FUNCT_7:32

.= Ch2 . o01 by A40, FUNCT_7:32

.= Ch1 . o01 by A40, FUNCT_7:32

.= the Charact of B . o01 by A40, FUNCT_7:32 ;

thus (Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . {} = (Den (o01,B)) . {} by A41

.= (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {}

.= TRUE by A4 ; :: thesis: for x, y being boolean object holds

( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*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 B,Ch6 #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = x '&' y )

A42: Ch6 . o02 = Ch5 . o02 by A40, FUNCT_7:32

.= Ch4 . o02 by A40, FUNCT_7:32

.= Ch3a . o02 by A40, FUNCT_7:32

.= Ch3 . o02 by A40, FUNCT_7:32

.= Ch2 . o02 by A40, FUNCT_7:32

.= Ch1 . o02 by A40, FUNCT_7:32

.= the Charact of B . o02 by A40, FUNCT_7:32 ;

thus (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x*> = (Den (o02,B)) . <*x*> by A42

.= 'not' x by A4 ; :: thesis: (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = x '&' y

A44: Ch6 . o03 = Ch5 . o03 by A40, FUNCT_7:32

.= Ch4 . o03 by A40, FUNCT_7:32

.= Ch3a . o03 by A40, FUNCT_7:32

.= Ch3 . o03 by A40, FUNCT_7:32

.= Ch2 . o03 by A40, FUNCT_7:32

.= Ch1 . o03 by A40, FUNCT_7:32

.= the Charact of B . o03 by A40, FUNCT_7:32 ;

thus (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = (Den (o03,B)) . <*x,y*> by A44

.= x '&' y by A4 ; :: thesis: verum

end;thus the Sorts of MSAlgebra(# the Sorts of B,Ch6 #) . the bool-sort of S = BOOLEAN by A4; :: according to AOFA_A00:def 31 :: thesis: ( (Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . {} = TRUE & ( for x, y being boolean object holds

( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = x '&' y ) ) )

( o01 is_of_type {} , the bool-sort of S & o02 is_of_type <* the bool-sort of S*>, the bool-sort of S & o03 is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S ) by Def30;

then ( the_arity_of o01 = {} & the_result_sort_of o01 = the bool-sort of S & the_result_sort_of o02 = the bool-sort of S & the_result_sort_of o03 = the bool-sort of S & the_arity_of o02 = <* the bool-sort of S*> & the_arity_of o03 = <* the bool-sort of S, the bool-sort of S*> & len <* the bool-sort of S*> = 1 & len <*I,I*> = 2 & <*I,I*> . 1 = I & <* the bool-sort of S, the bool-sort of S*> . 1 = the bool-sort of S ) by FINSEQ_1:40, FINSEQ_1:44;

then A40: ( o01 <> o4 & o01 <> o3 & o01 <> o2 & o01 <> o1 & o01 <> o5 & o01 <> o6 & o02 <> o4 & o02 <> o3 & o02 <> o2 & o02 <> o1 & o02 <> o5 & o02 <> o6 & o03 <> o4 & o03 <> o3 & o03 <> o2 & o03 <> o1 & o03 <> o5 & o03 <> o6 & o01 <> o7 & o02 <> o7 & o03 <> o7 ) by A3;

A41: Ch6 . o01 = Ch5 . o01 by A40, FUNCT_7:32

.= Ch4 . o01 by A40, FUNCT_7:32

.= Ch3a . o01 by A40, FUNCT_7:32

.= Ch3 . o01 by A40, FUNCT_7:32

.= Ch2 . o01 by A40, FUNCT_7:32

.= Ch1 . o01 by A40, FUNCT_7:32

.= the Charact of B . o01 by A40, FUNCT_7:32 ;

thus (Den ((In (( the connectives of S . 1), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . {} = (Den (o01,B)) . {} by A41

.= (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {}

.= TRUE by A4 ; :: thesis: for x, y being boolean object holds

( (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*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 B,Ch6 #))) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = x '&' y )

A42: Ch6 . o02 = Ch5 . o02 by A40, FUNCT_7:32

.= Ch4 . o02 by A40, FUNCT_7:32

.= Ch3a . o02 by A40, FUNCT_7:32

.= Ch3 . o02 by A40, FUNCT_7:32

.= Ch2 . o02 by A40, FUNCT_7:32

.= Ch1 . o02 by A40, FUNCT_7:32

.= the Charact of B . o02 by A40, FUNCT_7:32 ;

thus (Den ((In (( the connectives of S . 2), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x*> = (Den (o02,B)) . <*x*> by A42

.= 'not' x by A4 ; :: thesis: (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = x '&' y

A44: Ch6 . o03 = Ch5 . o03 by A40, FUNCT_7:32

.= Ch4 . o03 by A40, FUNCT_7:32

.= Ch3a . o03 by A40, FUNCT_7:32

.= Ch3 . o03 by A40, FUNCT_7:32

.= Ch2 . o03 by A40, FUNCT_7:32

.= Ch1 . o03 by A40, FUNCT_7:32

.= the Charact of B . o03 by A40, FUNCT_7:32 ;

thus (Den ((In (( the connectives of S . 3), the carrier' of S)),MSAlgebra(# the Sorts of B,Ch6 #))) . <*x,y*> = (Den (o03,B)) . <*x,y*> by A44

.= x '&' y by A4 ; :: thesis: verum

take D ; :: thesis: D is n,J integer

take I ; :: according to AOFA_A00:def 49 :: thesis: ( I = J & the connectives of S . n is_of_type {} ,I & the Sorts of D . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

thus I = J by A3; :: thesis: ( the connectives of S . n is_of_type {} ,I & the Sorts of D . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

thus the connectives of S . n is_of_type {} ,I by A3; :: thesis: ( the Sorts of D . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

thus the Sorts of D . I = ( the V2() ManySortedSet of the carrier of S +* (I,INT)) . I by A3, A4, FUNCT_7:32

.= INT by A11, FUNCT_7:31 ; :: thesis: ( (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

A46: ( {} in {{}} & 0 -tuples_on INT = {(<*> INT)} ) by TARSKI:def 1, FINSEQ_2:94;

Ch6 . o1 = Ch5 . o1 by A3, FUNCT_7:32

.= g0 by A39, FUNCT_7:31 ;

hence (Den ((In (( the connectives of S . n), the carrier' of S)),D)) . {} = 0 ; :: thesis: ( (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 & ( for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )

Ch6 . o2 = g1 by A39, FUNCT_7:31;

hence (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),D)) . {} = 1 by A46, FUNCOP_1:7; :: thesis: for i, j being Integer holds

( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

let i, j be Integer; :: thesis: ( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

( len <*I*> = 1 & len <*I,I*> = 2 ) by FINSEQ_1:40, FINSEQ_1:44;

then A48: ( o3 <> o4 & o3 <> o5 & o3 <> o6 & o3 <> o1 & o3 <> o2 & o3 <> o7 ) by A3;

A49: Ch6 . o3 = Ch5 . o3 by A13, A37, FUNCT_7:32

.= Ch4 . o3 by A13, A35, FUNCT_7:32

.= Ch3a . o3 by A48, FUNCT_7:32

.= Ch3 . o3 by A48, FUNCT_7:32

.= Ch2 . o3 by A48, FUNCT_7:32

.= Ch1 . o3 by A48, FUNCT_7:32

.= f1 by A39, FUNCT_7:31 ;

( In (o3, the carrier' of S) = o3 & i in INT & - i in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),D)) . <*i*> = In ((- i),INT) by A7, A49

.= - i ;

:: thesis: ( (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

A50: Ch6 . o4 = Ch5 . o4 by A19, A37, FUNCT_7:32

.= Ch4 . o4 by A19, A35, FUNCT_7:32

.= Ch3a . o4 by A3, FUNCT_7:32

.= Ch3 . o4 by A3, FUNCT_7:32

.= Ch2 . o4 by A3, FUNCT_7:32

.= f2 by A39, FUNCT_7:31 ;

( In (o4, the carrier' of S) = o4 & i in INT & j in INT & i + j in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),D)) . <*i,j*> = In ((i + j),INT) by A15, A50

.= i + j ;

:: thesis: ( (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

A51: ( o5 <> o6 & o5 <> o1 & o5 <> o2 & o5 <> o7 ) by A3;

A52: Ch6 . o5 = Ch5 . o5 by A51, FUNCT_7:32

.= Ch4 . o5 by A51, FUNCT_7:32

.= Ch3a . o5 by A51, FUNCT_7:32

.= Ch3 . o5 by A3, FUNCT_7:32

.= f3 by A39, FUNCT_7:31 ;

A53: ( In (o5, the carrier' of S) = o5 & i in INT & j in INT & i * j in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),D)) . <*i,j*> = In ((i * j),INT) by A21, A52

.= i * j ;

:: thesis: ( ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) )

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

A56: Ch6 . o7 =
Ch5 . o7
by A32, A37, FUNCT_7:32
assume
j <> 0
; :: thesis: (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div j

A54: ( o6 <> o1 & o6 <> o2 & o6 <> o7 ) by A3;

A55: Ch6 . o6 = Ch5 . o6 by A54, FUNCT_7:32

.= Ch4 . o6 by A54, FUNCT_7:32

.= Ch3a . o6 by A54, FUNCT_7:32

.= fa by A39, FUNCT_7:31 ;

( In (o6, the carrier' of S) = o6 & i in INT & j in INT & i div j in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = In ((i div j),INT) by A26, A55

.= i div j ;

:: thesis: verum

end;A54: ( o6 <> o1 & o6 <> o2 & o6 <> o7 ) by A3;

A55: Ch6 . o6 = Ch5 . o6 by A54, FUNCT_7:32

.= Ch4 . o6 by A54, FUNCT_7:32

.= Ch3a . o6 by A54, FUNCT_7:32

.= fa by A39, FUNCT_7:31 ;

( In (o6, the carrier' of S) = o6 & i in INT & j in INT & i div j in INT ) by INT_1:def 2;

hence (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = In ((i div j),INT) by A26, A55

.= i div j ;

:: thesis: verum

.= Ch4 . o7 by A32, A35, FUNCT_7:32

.= f4 by A39, FUNCT_7:31 ;

reconsider p = <*i,j*> as Element of 2 -tuples_on INT by A53, FINSEQ_2:101;

dom <*i,j*> = Seg 2 by FINSEQ_1:89;

then ( 1 in dom <*i,j*> & 2 in dom <*i,j*> ) ;

then A57: ( p /. 1 = p . 1 & p /. 2 = p . 2 & p . 1 = i & p . 2 = j ) by FINSEQ_1:44, PARTFUN1:def 6;

A58: ( In (o7, the carrier' of S) = o7 & i in INT & j in INT & ( i > j implies IFGT (i,j,FALSE,TRUE) = FALSE ) & ( i <= j implies IFGT (i,j,FALSE,TRUE) = TRUE ) & FALSE in BOOLEAN & TRUE in BOOLEAN ) by INT_1:def 2, XXREAL_0:def 11;

thus (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = H

.= IFGT (i,j,FALSE,TRUE) by A58, A57 ; :: thesis: verum