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 non-empty ManySortedSet of the carrier of S;
set A = the non-empty 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 non-empty 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₁( 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₁(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 non-empty ManySortedSet of the carrier of S +* (I,INT)) = the carrier of S & dom the non-empty 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 non-empty 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₂( 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₂(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₃( 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₃(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₄( 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₄(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₅( 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₅(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 )

proof

thus the Sorts of MSAlgebra(# the Sorts of B,Ch6 #) is non-empty ; :: 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;

then reconsider D = MSAlgebra(# the Sorts of B,Ch6 #) as strict non-empty bool-correct MSAlgebra over S ;
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 non-empty 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)

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;

A56: Ch6 . o7 = Ch5 . o7 by A32, A37, FUNCT_7:32
.= 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 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₅(p) by A56, A31
.= IFGT (i,j,FALSE,TRUE) by A58, A57 ; :: thesis: verum