let I, N be set ; for S being non empty non void 1,I,N -array ConnectivesSignature
for Y being non empty set
for X being V2() ManySortedSet of Y st ( the ResultSort of S . ( the connectives of S . 2) nin Y or X . ( the ResultSort of S . ( the connectives of S . 2)) = (X . I) ^omega ) & X . N = INT & I in Y holds
ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates X )
let S be non empty non void 1,I,N -array ConnectivesSignature ; for Y being non empty set
for X being V2() ManySortedSet of Y st ( the ResultSort of S . ( the connectives of S . 2) nin Y or X . ( the ResultSort of S . ( the connectives of S . 2)) = (X . I) ^omega ) & X . N = INT & I in Y holds
ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates X )
let A be non empty set ; for X being V2() ManySortedSet of A st ( the ResultSort of S . ( the connectives of S . 2) nin A or X . ( the ResultSort of S . ( the connectives of S . 2)) = (X . I) ^omega ) & X . N = INT & I in A holds
ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates X )
let V be V2() ManySortedSet of A; ( ( the ResultSort of S . ( the connectives of S . 2) nin A or V . ( the ResultSort of S . ( the connectives of S . 2)) = (V . I) ^omega ) & V . N = INT & I in A implies ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates V ) )
assume A1:
( the ResultSort of S . ( the connectives of S . 2) nin A or V . ( the ResultSort of S . ( the connectives of S . 2)) = (V . I) ^omega )
; ( not V . N = INT or not I in A or ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates V ) )
assume A2:
( V . N = INT & I in A )
; ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates V )
set X0 = the V2() ManySortedSet of the carrier of S;
set X = the V2() ManySortedSet of the carrier of S +* (V | the carrier of S);
reconsider X = the V2() ManySortedSet of the carrier of S +* (V | the carrier of S) as V2() ManySortedSet of the carrier of S ;
A3:
len the connectives of S >= 1 + 3
by Def50;
consider J, K, L being Element of S such that
A4:
( L = I & K = N & J <> L & J <> K & the connectives of S . 1 is_of_type <*J,K*>,L & the connectives of S . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (1 + 2) is_of_type <*J*>,K & the connectives of S . (1 + 3) is_of_type <*K,L*>,J )
by Def50;
A5:
( J nin A or V . J = (V . L) ^omega )
by A1, A4;
set Z = X +* (N,INT);
set Y = (X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega));
set O = the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S;
A6:
( dom V = A & dom X = the carrier of S )
by PARTFUN1:def 2;
then A7:
dom (V | the carrier of S) = A /\ the carrier of S
by RELAT_1:61;
then
I in dom (V | the carrier of S)
by A2, A4, XBOOLE_0:def 4;
then A8: X . I =
(V | the carrier of S) . I
by FUNCT_4:13
.=
V . I
by A4, FUNCT_1:49
;
N in dom V
by A2, FUNCT_1:def 2;
then
N in dom (V | the carrier of S)
by A6, A7, A4, XBOOLE_0:def 4;
then A9: X . N =
(V | the carrier of S) . N
by FUNCT_4:13
.=
V . N
by A4, FUNCT_1:49
;
deffunc H1( Function) -> object = IFIN (($1 . 2),(proj1 ($1 . 1)),($1 .. (1,($1 . 2))), the Element of ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L);
( N = I or N <> I )
;
then A10:
( (X +* (N,INT)) . I = X . I or ( (X +* (N,INT)) . I = INT & X . I = INT ) )
by A2, A4, A9, A6, FUNCT_7:31, FUNCT_7:32;
consider f being Function such that
A11:
( dom f = product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K)*> & ( for x being Element of product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K)*> holds f . x = H1(x) ) )
from FUNCT_1:sch 4();
A12:
( dom ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) = the carrier of S & dom (X +* (N,INT)) = the carrier of S & dom X = the carrier of S )
by PARTFUN1:def 2;
then A13:
( ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L = (X +* (N,INT)) . L & (X +* (N,INT)) . K = INT )
by A4, FUNCT_7:31, FUNCT_7:32;
then A14:
( ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J = (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K = INT )
by A12, A4, FUNCT_7:31, FUNCT_7:32;
rng f c= ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L
proof
let x be
object ;
TARSKI:def 3 ( not x in rng f or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L )
assume
x in rng f
;
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L
then consider y being
object such that A15:
(
y in dom f &
x = f . y )
by FUNCT_1:def 3;
reconsider y =
y as
Element of
product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K)*> by A11, A15;
A16:
x = H1(
y)
by A11, A15;
consider a,
b being
object such that A17:
(
a in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J &
b in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K &
y = <*a,b*> )
by FINSEQ_3:124;
reconsider a =
a as
Element of
(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega by A13, A17, A12, FUNCT_7:31;
A18:
(
a = y . 1 &
b = y . 2 &
a is
XFinSequence of
((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L )
by A17, FINSEQ_1:44;
end;
then reconsider f = f as Function of (product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K)*>),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) by A11, FUNCT_2:2;
1 <= len the connectives of S
by A3, XXREAL_0:2;
then A20:
1 in dom the connectives of S
by FINSEQ_3:25;
then reconsider o1 = the connectives of S . 1 as OperSymbol of S by FUNCT_1:102;
A21:
( the Arity of S . o1 = <*J,K*> & the ResultSort of S . o1 = L )
by A4;
<*J,K*> in the carrier of S *
by FINSEQ_1:def 11;
then
( (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) . ( the Arity of S . o1) = product (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*J,K*>) & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*J,K*> = <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K)*> & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . ( the ResultSort of S . o1) = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L )
by A21, A12, FINSEQ_2:def 5, FINSEQ_2:125;
then
( ((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o1 = product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K)*> & (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o1 = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L )
by FUNCT_2:15;
then reconsider f = f as Function of (((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o1),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o1) ;
deffunc H2( Element of product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*>) -> set = ($1 . 1) +* (($1 . 2),($1 . 3));
consider g being Function such that
A22:
( dom g = product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> & ( for x being Element of product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> holds g . x = H2(x) ) )
from FUNCT_1:sch 4();
rng g c= ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J
proof
let x be
object ;
TARSKI:def 3 ( not x in rng g or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
assume
x in rng g
;
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J
then consider y being
object such that A23:
(
y in dom g &
x = g . y )
by FUNCT_1:def 3;
reconsider y =
y as
Element of
product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> by A22, A23;
consider a,
b,
c being
object such that A24:
(
a in (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega &
b in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K &
c in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L &
y = <*a,b,c*> )
by FINSEQ_3:125;
reconsider a =
a as
XFinSequence of
((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L by A24;
reconsider c =
c as
Element of
((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L by A24;
A25:
(
a = y . 1 &
b = y . 2 &
c = y . 3 )
by A24, FINSEQ_1:45;
A26:
x = a +* (
b,
c)
by A25, A22, A23;
x is
XFinSequence of
((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L
by A26;
then
x in (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega
by AFINSQ_1:def 7;
hence
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J
by A14;
verum
end;
then reconsider g = g as Function of (product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*>),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J) by A14, A22, FUNCT_2:2;
2 <= len the connectives of S
by A3, XXREAL_0:2;
then A27:
2 in dom the connectives of S
by FINSEQ_3:25;
then reconsider o2 = the connectives of S . 2 as OperSymbol of S by FUNCT_1:102;
A28:
( the Arity of S . o2 = <*J,K,L*> & the ResultSort of S . o2 = J )
by A4;
<*J,K,L*> in the carrier of S *
by FINSEQ_1:def 11;
then
( (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) . ( the Arity of S . o2) = product (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*J,K,L*>) & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*J,K,L*> = <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . ( the ResultSort of S . o2) = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
by A28, A12, FINSEQ_2:def 5, FINSEQ_2:126;
then
( ((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o2 = product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> & (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o2 = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
by FUNCT_2:15;
then reconsider g = g as Function of (((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o2),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o2) ;
deffunc H3( Element of product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega)*>) -> set = card ($1 . 1);
consider h being Function such that
A29:
( dom h = product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega)*> & ( for x being Element of product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega)*> holds h . x = H3(x) ) )
from FUNCT_1:sch 4();
rng h c= ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K
proof
let x be
object ;
TARSKI:def 3 ( not x in rng h or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K )
assume
x in rng h
;
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K
then consider y being
object such that A30:
(
y in dom h &
x = h . y )
by FUNCT_1:def 3;
reconsider y =
y as
Element of
product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega)*> by A29, A30;
A31:
x = H3(
y)
by A29, A30;
consider a being
object such that A32:
(
a in (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega &
y = <*a*> )
by FINSEQ_3:123;
reconsider a =
a as
finite 0 -based array of
((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L by A32;
x = len a
by A31, A32, FINSEQ_1:40;
hence
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K
by A14, INT_1:def 2;
verum
end;
then reconsider h = h as Function of (product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J)*>),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K) by A14, A29, FUNCT_2:2;
3 <= len the connectives of S
by A3, XXREAL_0:2;
then A33:
3 in dom the connectives of S
by FINSEQ_3:25;
then reconsider o3 = the connectives of S . 3 as OperSymbol of S by FUNCT_1:102;
A34:
( the Arity of S . o3 = <*J*> & the ResultSort of S . o3 = K )
by A4;
<*J*> in the carrier of S *
by FINSEQ_1:def 11;
then
( (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) . ( the Arity of S . o3) = product (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*J*>) & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*J*> = <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J)*> & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . ( the ResultSort of S . o3) = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K )
by A34, A12, FINSEQ_2:def 5, FINSEQ_2:34;
then
( ((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o3 = product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J)*> & (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o3 = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K )
by FUNCT_2:15;
then reconsider h = h as Function of (((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o3),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o3) ;
deffunc H4( Element of product <*INT,(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*>) -> object = IFGT (0,($1 . 1),{},(($1 . 1) --> ($1 . 2)));
consider j being Function such that
A35:
( dom j = product <*INT,(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> & ( for x being Element of product <*INT,(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> holds j . x = H4(x) ) )
from FUNCT_1:sch 4();
rng j c= ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J
proof
let x be
object ;
TARSKI:def 3 ( not x in rng j or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
assume
x in rng j
;
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J
then consider y being
object such that A36:
(
y in dom j &
x = j . y )
by FUNCT_1:def 3;
reconsider y =
y as
Element of
product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> by A35, A36, A13, A4, FUNCT_7:32;
consider b,
c being
object such that A37:
(
b in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K &
c in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L &
y = <*b,c*> )
by FINSEQ_3:124;
reconsider c =
c as
Element of
((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L by A37;
reconsider b =
b as
Integer by A37, A14;
A38:
(
b = y . 1 &
c = y . 2 )
by A37, FINSEQ_1:44;
x = IFGT (
0,
b,
{},
((Segm b) --> c))
by A38, A35, A36;
then
(
x = {} or (
b >= 0 &
x = (Segm b) --> c & ( not
b is
negative implies
b is
Nat ) ) )
by XXREAL_0:def 11;
then
(
x = <%> (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) or ex
b being non
negative Nat st
x = b --> c )
;
hence
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J
by A14, AFINSQ_1:def 7;
verum
end;
then reconsider j = j as Function of (product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*>),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J) by A14, A35, FUNCT_2:2;
A39:
4 in dom the connectives of S
by A3, FINSEQ_3:25;
then reconsider o4 = the connectives of S . 4 as OperSymbol of S by FUNCT_1:102;
A40:
( the Arity of S . o4 = <*K,L*> & the ResultSort of S . o4 = J )
by A4;
<*K,L*> in the carrier of S *
by FINSEQ_1:def 11;
then
( (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) . ( the Arity of S . o4) = product (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*K,L*>) & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * <*K,L*> = <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . ( the ResultSort of S . o4) = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
by A40, A12, FINSEQ_2:def 5, FINSEQ_2:125;
then
( ((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o4 = product <*(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> & (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o4 = ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
by FUNCT_2:15;
then reconsider j = j as Function of (((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . o4),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . o4) ;
set U = ((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j);
A41:
( dom the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S = the carrier' of S & dom ( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) = the carrier' of S & dom (( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) = the carrier' of S & dom (((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) = the carrier' of S & dom ((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) = the carrier' of S )
by PARTFUN1:def 2;
( card ( the Arity of S . o1) = 2 & card ( the Arity of S . o2) = 3 & card ( the Arity of S . o3) = 1 & card ( the Arity of S . o4) = 2 )
by A21, A28, A34, A40, CARD_1:def 7;
then A42:
( o1 <> o2 & o2 <> o3 & o3 <> o1 & o1 <> o4 & o2 <> o4 & o3 <> o4 )
by A4;
A43: (((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . o1 =
((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) . o1
by A42, FUNCT_7:32
.=
(( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) . o1
by A42, FUNCT_7:32
.=
( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) . o1
by A42, FUNCT_7:32
.=
f
by A41, FUNCT_7:31
;
A44: (((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . o2 =
((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) . o2
by A42, FUNCT_7:32
.=
(( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) . o2
by A42, FUNCT_7:32
.=
g
by A41, FUNCT_7:31
;
A45: (((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . o3 =
((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) . o3
by A42, FUNCT_7:32
.=
h
by A41, FUNCT_7:31
;
A46:
(((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . o4 = j
by A41, FUNCT_7:31;
((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j) is ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S
proof
let x be
object ;
PBOOLE:def 15 ( not x in the carrier' of S or (((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . x is Element of bool [:(((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . x),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . x):] )
assume
x in the
carrier' of
S
;
(((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . x is Element of bool [:(((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . x),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . x):]
then reconsider o =
x as
OperSymbol of
S ;
per cases
( o = o1 or o = o2 or o = o3 or o = o4 or ( o <> o1 & o <> o2 & o <> o3 & o <> o4 ) )
;
suppose
(
o = o1 or
o = o2 or
o = o3 or
o = o4 )
;
(((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . x is Element of bool [:(((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . x),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . x):]hence
(((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . x is
Function of
(((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . x),
((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . x)
by A43, A44, A45, A41, FUNCT_7:31;
verum end; suppose A47:
(
o <> o1 &
o <> o2 &
o <> o3 &
o <> o4 )
;
(((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . x is Element of bool [:(((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . x),((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . x):](((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . o =
((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) . o
by A47, FUNCT_7:32
.=
(( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) . o
by A47, FUNCT_7:32
.=
( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) . o
by A47, FUNCT_7:32
.=
the
ManySortedFunction of
(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the
Arity of
S,
((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the
ResultSort of
S . o
by A47, FUNCT_7:32
;
hence
(((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j)) . x is
Function of
(((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S) . x),
((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S) . x)
;
verum end; end;
end;
then reconsider U = ((( the ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S +* (o1,f)) +* (o2,g)) +* (o3,h)) +* (o4,j) as ManySortedFunction of (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) #) * the Arity of S,((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) * the ResultSort of S ;
set A = MSAlgebra(# ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))),U #);
MSAlgebra(# ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))),U #) is non-empty
;
then reconsider A = MSAlgebra(# ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))),U #) as strict non-empty MSAlgebra over S ;
take
A
; ( A is 1,I,N -array & the Sorts of A tolerates V )
thus
A is 1,I,N -array
the Sorts of A tolerates Vproof
take
J
;
AOFA_A00:def 51 ex K being Element of S st
( K = I & the connectives of S . 1 is_of_type <*J,N*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . N = INT & ( for a being finite 0 -based array of the Sorts of A . K holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,K st i >= 0 holds
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
take
L
;
( L = I & the connectives of S . 1 is_of_type <*J,N*>,L & the Sorts of A . J = ( the Sorts of A . L) ^omega & the Sorts of A . N = INT & ( for a being finite 0 -based array of the Sorts of A . L holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,L st i >= 0 holds
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
thus
L = I
by A4;
( the connectives of S . 1 is_of_type <*J,N*>,L & the Sorts of A . J = ( the Sorts of A . L) ^omega & the Sorts of A . N = INT & ( for a being finite 0 -based array of the Sorts of A . L holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,L st i >= 0 holds
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
thus
the
connectives of
S . 1
is_of_type <*J,N*>,
L
by A4;
( the Sorts of A . J = ( the Sorts of A . L) ^omega & the Sorts of A . N = INT & ( for a being finite 0 -based array of the Sorts of A . L holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,L st i >= 0 holds
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
thus
( the
Sorts of
A . J = ( the Sorts of A . L) ^omega & the
Sorts of
A . N = INT )
by A4, A13, A12, FUNCT_7:31, FUNCT_7:32;
( ( for a being finite 0 -based array of the Sorts of A . L holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,L st i >= 0 holds
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
hereby for i being Integer
for x being Element of A,L st i >= 0 holds
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x
let a be
finite 0 -based array of the
Sorts of
A . L;
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a )A48:
a in (((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega
by AFINSQ_1:def 7;
hereby (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a
let i be
Integer;
( i in dom a implies ( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) )assume A49:
i in dom a
;
( (Den (( the connectives of S /. 1),A)) . <*a,i*> = a . i & ( for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) )A50:
i in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . N
by A4, A14, INT_1:def 2;
then A51:
<*a,i*> in product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . N)*>
by A48, FINSEQ_3:124;
A52:
(
<*a,i*> . 1
= a &
<*a,i*> . 2
= i )
by FINSEQ_1:44;
the
connectives of
S /. 1
= o1
by A20, PARTFUN1:def 6;
hence (Den (( the connectives of S /. 1),A)) . <*a,i*> =
H1(
<*a,i*>)
by A4, A11, A14, A43, A51
.=
<*a,i*> .. (1,
i)
by A52, A49, MATRIX_7:def 1
.=
a . i
by A52, Th5
;
for x being Element of A,L holds (Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x)let x be
Element of
A,
L;
(Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (i,x)A53:
<*a,i,x*> in product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . N),(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*>
by A48, A50, FINSEQ_3:125;
A54:
(
<*a,i,x*> . 1
= a &
<*a,i,x*> . 2
= i &
<*a,i,x*> . 3
= x )
by FINSEQ_1:45;
the
connectives of
S /. 2
= o2
by A27, PARTFUN1:def 6;
hence
(Den (( the connectives of S /. (1 + 1)),A)) . <*a,i,x*> = a +* (
i,
x)
by A4, A22, A44, A53, A54;
verum
end; A55:
<*a*> in product <*((((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L) ^omega)*>
by A48, FINSEQ_3:123;
A56:
<*a*> . 1
= a
by FINSEQ_1:40;
the
connectives of
S /. 3
= o3
by A33, PARTFUN1:def 6;
hence
(Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a
by A29, A45, A55, A56;
verum
end;
let i be
Integer;
for x being Element of A,L st i >= 0 holds
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> xlet x be
Element of
A,
L;
( i >= 0 implies (Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x )
assume A57:
i >= 0
;
(Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x
A58:
o4 = the
connectives of
S /. (1 + 3)
by A39, PARTFUN1:def 6;
(
i in INT &
x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L )
by INT_1:def 2;
then
(
<*i,x*> in product <*INT,(((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L)*> &
<*i,x*> . 1
= i &
<*i,x*> . 2
= x )
by FINSEQ_1:44, FINSEQ_3:124;
hence (Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> =
IFGT (
0,
i,
{},
((Segm i) --> x))
by A35, A46, A58
.=
(Segm i) --> x
by A57, XXREAL_0:def 11
;
verum
end;
thus
the Sorts of A tolerates V
verum