let n be Nat; 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 ; ( 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
; 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 ; ( 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
; 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 H1( 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*> = H1(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 H2( 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*> = H2(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 H3( 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*> = H3(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 H4( 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*> = H4(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 H5( 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 = H5(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
V2()
;
MSUALG_1:def 3 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;
AOFA_A00:def 31 ( (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
;
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 ;
( (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
;
(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
;
verum
end;
then reconsider D = MSAlgebra(# the Sorts of B,Ch6 #) as strict non-empty bool-correct MSAlgebra over S ;
take
D
; D is n,J integer
take
I
; AOFA_A00:def 49 ( 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; ( 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; ( 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
; ( (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
; ( (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; 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; ( (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
;
( (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
;
( (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
;
( ( 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 (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),D)) . <*i,j*> = IFGT (i,j,FALSE,TRUE)
assume
j <> 0
;
(Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),D)) . <*i,j*> = i div jA54:
(
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
;
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 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*> =
H5(p)
by A56, A31
.=
IFGT (i,j,FALSE,TRUE)
by A58, A57
; verum