let I, N be set ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: ( 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 ) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L )
assume x in rng f ; :: thesis: 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;
per cases ( y . 2 in proj1 (y . 1) or y . 2 nin proj1 (y . 1) ) ;
suppose A19: y . 2 in proj1 (y . 1) ; :: thesis: x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L
then x = y .. (1,(y . 2)) by A16, MATRIX_7:def 1
.= a . b by A18, Th5 ;
hence x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L by A18, A19, FUNCT_1:102; :: thesis: verum
end;
suppose y . 2 nin proj1 (y . 1) ; :: thesis: x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L
then x = the Element of ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L by A16, MATRIX_7:def 1;
hence x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . L ; :: thesis: verum
end;
end;
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 ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
assume x in rng g ; :: thesis: 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; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in rng h or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . K )
assume x in rng h ; :: thesis: 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; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in rng j or x in ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . J )
assume x in rng j ; :: thesis: 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; :: thesis: 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 ; :: according to PBOOLE:def 15 :: thesis: ( 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 ; :: thesis: (((( 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 ) ; :: thesis: (((( 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; :: thesis: verum
end;
suppose A47: ( o <> o1 & o <> o2 & o <> o3 & o <> o4 ) ; :: thesis: (((( 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) ; :: thesis: 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 ; :: thesis: ( A is 1,I,N -array & the Sorts of A tolerates V )
thus A is 1,I,N -array :: thesis: the Sorts of A tolerates V
proof
take J ; :: according to AOFA_A00:def 51 :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( ( 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 :: thesis: 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; :: thesis: ( ( 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 :: thesis: (Den (( the connectives of S /. (1 + 2)),A)) . <*a*> = card a
let i be Integer; :: thesis: ( 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 ; :: thesis: ( (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 ;
:: thesis: 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; :: thesis: (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; :: thesis: 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; :: thesis: verum
end;
let i be Integer; :: thesis: 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 x be Element of A,L; :: thesis: ( i >= 0 implies (Den (( the connectives of S /. (1 + 3)),A)) . <*i,x*> = (Segm i) --> x )
assume A57: i >= 0 ; :: thesis: (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 ;
:: thesis: verum
end;
thus the Sorts of A tolerates V :: thesis: verum
proof
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the Sorts of A) /\ (proj1 V) or the Sorts of A . x = V . x )
assume A59: x in (dom the Sorts of A) /\ (dom V) ; :: thesis: the Sorts of A . x = V . x
then x in the carrier of S /\ (dom V) by PARTFUN1:def 2;
then A60: x in dom (V | the carrier of S) by RELAT_1:61;
then A61: X . x = (V | the carrier of S) . x by FUNCT_4:13
.= V . x by A60, FUNCT_1:47 ;
per cases ( ( x <> N & x <> J ) or x = N or x = J ) ;
suppose ( x <> N & x <> J ) ; :: thesis: the Sorts of A . x = V . x
then ( (X +* (N,INT)) . x = X . x & ((X +* (N,INT)) +* (J,(((X +* (N,INT)) . L) ^omega))) . x = (X +* (N,INT)) . x ) by FUNCT_7:32;
hence the Sorts of A . x = V . x by A61; :: thesis: verum
end;
suppose x = N ; :: thesis: the Sorts of A . x = V . x
hence the Sorts of A . x = V . x by A2, A13, A4, FUNCT_7:32; :: thesis: verum
end;
suppose A62: x = J ; :: thesis: the Sorts of A . x = V . x
then ( x nin dom V or ( x in dom V & V . x = (V . L) ^omega ) ) by A5, PARTFUN1:def 2;
hence the Sorts of A . x = V . x by A59, A10, A62, A12, A4, FUNCT_7:31, XBOOLE_0:def 4, A8; :: thesis: verum
end;
end;
end;