let Q be non-empty MSSubAlgebra of A; :: thesis: Q is 11,1,1 -array
set I = the integer SortSymbol of S;
A1: the Sorts of Q . the integer SortSymbol of S = INT by AOFA_A00:55;
then reconsider 00 = 0 as Element of Q, the integer SortSymbol of S by INT_1:def 2;
reconsider 0a = 00 as Element of A, the integer SortSymbol of S by Th2;
consider J, K being Element of S such that
A2: ( K = 1 & the connectives of S . 11 is_of_type <*J,1*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . 1 = 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 /. 11),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. (11 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (11 + 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 /. (11 + 3)),A)) . <*i,x*> = (Segm i) --> x ) ) by AOFA_A00:def 52;
consider J1, K1, L1 being Element of S such that
A3: ( L1 = 1 & K1 = 1 & J1 <> L1 & J1 <> K1 & the connectives of S . 11 is_of_type <*J1,K1*>,L1 & the connectives of S . (11 + 1) is_of_type <*J1,K1,L1*>,J1 & the connectives of S . (11 + 2) is_of_type <*J1*>,K1 & the connectives of S . (11 + 3) is_of_type <*K1,L1*>,J1 ) by AOFA_A00:def 51;
A4: the integer SortSymbol of S = 1 by AOFA_A00:def 40;
A5: ( the_array_sort_of S = J & the_array_sort_of S = J1 ) by A3, A2, Th71;
A6: for a being finite 0 -based array of INT holds a in the Sorts of Q . (the_array_sort_of S)
proof
let a be finite 0 -based array of INT ; :: thesis: a in the Sorts of Q . (the_array_sort_of S)
set o = In (( the connectives of S . 14), the carrier' of S);
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 14 in dom the connectives of S by FINSEQ_3:25;
then In (( the connectives of S . 14), the carrier' of S) = the connectives of S . 14 by FUNCT_1:102, SUBSET_1:def 8;
then the_arity_of (In (( the connectives of S . 14), the carrier' of S)) = <*K,K*> by A3, A2;
then A7: ( Args ((In (( the connectives of S . 14), the carrier' of S)),Q) = product <*INT,INT*> & 0 in INT ) by A2, A4, A1, Th23, INT_1:def 2;
per cases ( len a = 0 or len a <> 0 ) ;
suppose len a = 0 ; :: thesis: a in the Sorts of Q . (the_array_sort_of S)
then a = <%> INT ;
then a = init.array (0a,0a) by Th72
.= init.array (00,00) by A7, FINSEQ_3:124, EQUATION:19 ;
hence a in the Sorts of Q . (the_array_sort_of S) ; :: thesis: verum
end;
suppose A8: len a <> 0 ; :: thesis: a in the Sorts of Q . (the_array_sort_of S)
deffunc H1( array, Integer, set ) -> set = S +* (A,c3);
deffunc H2( Integer) -> set = a . S;
set j = len a;
A9: for a being finite 0 -based array of INT
for i being Nat st 1 <= i & i < len a holds
for x being Element of INT holds H1(a,i,x) is finite 0 -based array of INT ;
set B = (Segm (len a)) --> (a . 0);
A10: (Segm (len a)) --> (a . 0) is finite 0 -based array of INT ;
A11: for i being Nat st i < len a holds
H2(i) in INT by AFINSQ_1:86, FUNCT_1:102;
consider f being FinSequence of INT ^omega such that
A12: ( len f = len a & ( f . 1 = (Segm (len a)) --> (a . 0) or len a = 0 ) & ( for i being Nat st 1 <= i & i < len a holds
f . (i + 1) = H1(f . i,i,H2(i)) ) ) from AOFA_A01:sch 1(A9, A10, A11);
reconsider f = f as Function-yielding FinSequence of INT ^omega ;
defpred S1[ Nat] means ( S <= len a implies ( ( S <> 0 implies len (f . S) = len a ) & ( for i being Nat st i < S holds
a . i = (f . S) . i ) ) );
A13: S1[ 0 ] ;
A14: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A15: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
assume A16: i + 1 <= len a ; :: thesis: ( ( i + 1 <> 0 implies len (f . (i + 1)) = len a ) & ( for i being Nat st i < i + 1 holds
a . i = (f . (i + 1)) . i ) )
per cases ( i = 0 or i > 0 ) ;
suppose A17: i = 0 ; :: thesis: ( ( i + 1 <> 0 implies len (f . (i + 1)) = len a ) & ( for i being Nat st i < i + 1 holds
a . i = (f . (i + 1)) . i ) )
thus ( i + 1 <> 0 implies len (f . (i + 1)) = len a ) by A12, A16, A17; :: thesis: for i being Nat st i < i + 1 holds
a . i = (f . (i + 1)) . i
let k be Nat; :: thesis: ( k < i + 1 implies a . k = (f . (i + 1)) . k )
assume k < i + 1 ; :: thesis: a . k = (f . (i + 1)) . k
then ( k <= 0 & k >= 0 ) by A17, NAT_1:13;
then A18: k = 0 ;
then k < len a by A16;
hence a . k = (f . (i + 1)) . k by A17, A12, A18, FUNCOP_1:7, AFINSQ_1:86; :: thesis: verum
end;
suppose A19: i > 0 ; :: thesis: ( ( i + 1 <> 0 implies len (f . (i + 1)) = len a ) & ( for i being Nat st i < i + 1 holds
a . i = (f . (i + 1)) . i ) )
then A20: ( i >= 0 + 1 & i < len a ) by A16, NAT_1:13;
then A21: f . (i + 1) = H1(f . i,i,H2(i)) by A12;
thus ( i + 1 <> 0 implies len (f . (i + 1)) = len a ) by A15, A19, A21, A16, NAT_1:13, FUNCT_7:30; :: thesis: for i being Nat st i < i + 1 holds
a . i = (f . (i + 1)) . i
let k be Nat; :: thesis: ( k < i + 1 implies a . k = (f . (i + 1)) . k )
assume k < i + 1 ; :: thesis: a . k = (f . (i + 1)) . k
then A22: ( k <= i & k < len a ) by A16, XXREAL_0:2, NAT_1:13;
per cases ( k = i or k < i ) by A22, XXREAL_0:1;
suppose k = i ; :: thesis: a . k = (f . (i + 1)) . k
then ( f . (i + 1) = (f . i) +* (k,(a . k)) & k in dom (f . i) ) by A15, A12, A20, AFINSQ_1:86;
hence a . k = (f . (i + 1)) . k by FUNCT_7:31; :: thesis: verum
end;
suppose A23: k < i ; :: thesis: a . k = (f . (i + 1)) . k
A24: ( f . (i + 1) = (f . i) +* (i,(a . i)) & k in dom (f . i) ) by A20, A12, A15, A22, AFINSQ_1:86;
thus a . k = (f . i) . k by A15, A23, A16, NAT_1:13
.= (f . (i + 1)) . k by A23, A24, FUNCT_7:32 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
A25: for i being Nat holds S1[i] from NAT_1:sch 2(A13, A14);
then ( ( len a <> 0 implies len (f . (len a)) = len a ) & ( for i being Nat st i < len a holds
a . i = (f . (len a)) . i ) ) ;
then A26: f . (len a) = a by A8, AFINSQ_1:9;
defpred S2[ Nat] means ( 1 <= S & S <= len a implies f . S in the Sorts of Q . (the_array_sort_of S) );
A27: S2[ 0 ] ;
A28: now :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A29: S2[i] ; :: thesis: S2[i + 1]
thus S2[i + 1] :: thesis: verum
proof
assume A30: ( 1 <= i + 1 & i + 1 <= len a ) ; :: thesis: f . (i + 1) in the Sorts of Q . (the_array_sort_of S)
then A31: i < len a by NAT_1:13;
per cases ( i >= 1 or i = 0 ) by NAT_1:14;
suppose A32: i >= 1 ; :: thesis: f . (i + 1) in the Sorts of Q . (the_array_sort_of S)
then reconsider fi = f . i as Element of Q,(the_array_sort_of S) by A29, A30, NAT_1:13;
fi in the Sorts of A . J by A5, Th2;
then reconsider ff = fi as finite Sequence of INT by A2;
reconsider ii = i as Element of the Sorts of Q . the integer SortSymbol of S by A1, INT_1:def 2;
reconsider a = H2(i) as Element of the Sorts of Q . the integer SortSymbol of S by A1, A11, A30, NAT_1:13;
reconsider b = a, ia = ii as Element of the Sorts of A . the integer SortSymbol of S by Th2;
reconsider fj = fi as Element of A,(the_array_sort_of S) by Th2;
( f . (i + 1) = H1(f . i,i,H2(i)) & ( 1 = 0 + 1 implies i > 0 ) & f . i in the Sorts of Q . (the_array_sort_of S) ) by A29, A32, A12, A30, NAT_1:13;
then len (f . i) = len a by A31, A25;
then A33: i in dom ff by A31, AFINSQ_1:86;
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 12 <= len the connectives of S by XXREAL_0:2;
then 12 in dom the connectives of S by FINSEQ_3:25;
then A34: ( the connectives of S . 12 = the connectives of S /. 12 & the connectives of S . 12 in the carrier' of S ) by PARTFUN1:def 6, FUNCT_1:102;
then the_arity_of ( the connectives of S /. 12) = <*(the_array_sort_of S), the integer SortSymbol of S, the integer SortSymbol of S*> by A3, A4;
then A35: Args (( the connectives of S /. 12),Q) = product <*( the Sorts of Q . (the_array_sort_of S)),( the Sorts of Q . the integer SortSymbol of S),( the Sorts of Q . the integer SortSymbol of S)*> by Th24;
f . (i + 1) = ff +* (i,a) by A32, A12, A30, NAT_1:13
.= (Den (( the connectives of S /. 12),A)) . <*fj,ia,b*> by A4, A2, A33
.= (Den (( the connectives of S /. 12),Q)) . <*fi,ii,a*> by A35, FINSEQ_3:125, EQUATION:19
.= (fi,ii) <- a by A34, SUBSET_1:def 8 ;
hence f . (i + 1) in the Sorts of Q . (the_array_sort_of S) ; :: thesis: verum
end;
suppose A36: i = 0 ; :: thesis: f . (i + 1) in the Sorts of Q . (the_array_sort_of S)
reconsider a0 = a . 0, ii = len a as Element of Q, the integer SortSymbol of S by A1, INT_1:def 2;
reconsider b0 = a0, ia = ii as Element of A, the integer SortSymbol of S by Th2;
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 14 in dom the connectives of S by FINSEQ_3:25;
then A37: ( the connectives of S . 14 = the connectives of S /. 14 & the connectives of S . 14 in the carrier' of S ) by PARTFUN1:def 6, FUNCT_1:102;
then the_arity_of ( the connectives of S /. 14) = <* the integer SortSymbol of S, the integer SortSymbol of S*> by A3, A4;
then A38: Args (( the connectives of S /. 14),Q) = product <*( the Sorts of Q . the integer SortSymbol of S),( the Sorts of Q . the integer SortSymbol of S)*> by Th23;
f . (i + 1) = (Den (( the connectives of S /. 14),A)) . <*ia,b0*> by A36, A12, A8, A4, A2
.= (Den (( the connectives of S /. 14),Q)) . <*ii,a0*> by A38, FINSEQ_3:124, EQUATION:19
.= init.array (ii,a0) by A37, SUBSET_1:def 8 ;
hence f . (i + 1) in the Sorts of Q . (the_array_sort_of S) ; :: thesis: verum
end;
end;
end;
end;
A39: for i being Nat holds S2[i] from NAT_1:sch 2(A27, A28);
 0 < len a by A8;
then 0 + 1 <= len a by NAT_1:13;
hence a in the Sorts of Q . (the_array_sort_of S) by A26, A39; :: thesis: verum
end;
end;
end;
take J ; :: according to AOFA_A00:def 51 :: thesis: ex b1 being Element of the carrier of S st
( b1 = 1 & the connectives of S . 11 is_of_type <*J,1*>,b1 & the Sorts of Q . J = ( the Sorts of Q . b1) ^omega & the Sorts of Q . 1 = INT & ( for b2 being set holds
( ( for b3 being object holds
( not b3 in dom b2 or ( (Den (( the connectives of S /. 11),Q)) . <*b2,b3*> = b2 . b3 & ( for b4 being Element of the Sorts of Q . b1 holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*b2,b3,b4*> = b2 +* (b3,b4) ) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*b2*> = card b2 ) ) & ( for b2 being object
for b3 being Element of the Sorts of Q . b1 holds
( not 0 <= b2 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b2,b3*> = (Segm b2) --> b3 ) ) )
take K ; :: thesis: ( K = 1 & the connectives of S . 11 is_of_type <*J,1*>,K & the Sorts of Q . J = ( the Sorts of Q . K) ^omega & the Sorts of Q . 1 = INT & ( for b1 being set holds
( ( for b2 being object holds
( not b2 in dom b1 or ( (Den (( the connectives of S /. 11),Q)) . <*b1,b2*> = b1 . b2 & ( for b3 being Element of the Sorts of Q . K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*b1,b2,b3*> = b1 +* (b2,b3) ) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*b1*> = card b1 ) ) & ( for b1 being object
for b2 being Element of the Sorts of Q . K holds
( not 0 <= b1 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b1,b2*> = (Segm b1) --> b2 ) ) )
thus K = 1 by A2; :: thesis: ( the connectives of S . 11 is_of_type <*J,1*>,K & the Sorts of Q . J = ( the Sorts of Q . K) ^omega & the Sorts of Q . 1 = INT & ( for b1 being set holds
( ( for b2 being object holds
( not b2 in dom b1 or ( (Den (( the connectives of S /. 11),Q)) . <*b1,b2*> = b1 . b2 & ( for b3 being Element of the Sorts of Q . K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*b1,b2,b3*> = b1 +* (b2,b3) ) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*b1*> = card b1 ) ) & ( for b1 being object
for b2 being Element of the Sorts of Q . K holds
( not 0 <= b1 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b1,b2*> = (Segm b1) --> b2 ) ) )
thus the connectives of S . 11 is_of_type <*J,1*>,K by A2; :: thesis: ( the Sorts of Q . J = ( the Sorts of Q . K) ^omega & the Sorts of Q . 1 = INT & ( for b1 being set holds
( ( for b2 being object holds
( not b2 in dom b1 or ( (Den (( the connectives of S /. 11),Q)) . <*b1,b2*> = b1 . b2 & ( for b3 being Element of the Sorts of Q . K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*b1,b2,b3*> = b1 +* (b2,b3) ) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*b1*> = card b1 ) ) & ( for b1 being object
for b2 being Element of the Sorts of Q . K holds
( not 0 <= b1 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b1,b2*> = (Segm b1) --> b2 ) ) )
the Sorts of Q is MSSubset of A by MSUALG_2:def 9;
hence the Sorts of Q . J c= ( the Sorts of Q . K) ^omega by A1, A4, A2, PBOOLE:def 2, PBOOLE:def 18; :: according to XBOOLE_0:def 10 :: thesis: ( ( the Sorts of Q . K) ^omega c= the Sorts of Q . J & the Sorts of Q . 1 = INT & ( for b1 being set holds
( ( for b2 being object holds
( not b2 in dom b1 or ( (Den (( the connectives of S /. 11),Q)) . <*b1,b2*> = b1 . b2 & ( for b3 being Element of the Sorts of Q . K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*b1,b2,b3*> = b1 +* (b2,b3) ) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*b1*> = card b1 ) ) & ( for b1 being object
for b2 being Element of the Sorts of Q . K holds
( not 0 <= b1 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b1,b2*> = (Segm b1) --> b2 ) ) )
thus A40: ( the Sorts of Q . K) ^omega c= the Sorts of Q . J by A5, A6, A1, A4, A2; :: thesis: ( the Sorts of Q . 1 = INT & ( for b1 being set holds
( ( for b2 being object holds
( not b2 in dom b1 or ( (Den (( the connectives of S /. 11),Q)) . <*b1,b2*> = b1 . b2 & ( for b3 being Element of the Sorts of Q . K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*b1,b2,b3*> = b1 +* (b2,b3) ) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*b1*> = card b1 ) ) & ( for b1 being object
for b2 being Element of the Sorts of Q . K holds
( not 0 <= b1 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b1,b2*> = (Segm b1) --> b2 ) ) )
thus the Sorts of Q . 1 = INT by AOFA_A00:55, A4; :: thesis: ( ( for b1 being set holds
( ( for b2 being object holds
( not b2 in dom b1 or ( (Den (( the connectives of S /. 11),Q)) . <*b1,b2*> = b1 . b2 & ( for b3 being Element of the Sorts of Q . K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*b1,b2,b3*> = b1 +* (b2,b3) ) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*b1*> = card b1 ) ) & ( for b1 being object
for b2 being Element of the Sorts of Q . K holds
( not 0 <= b1 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b1,b2*> = (Segm b1) --> b2 ) ) )
hereby :: thesis: for b1 being object
for b2 being Element of the Sorts of Q . K holds
( not 0 <= b1 or (Den (( the connectives of S /. (11 + 3)),Q)) . <*b1,b2*> = (Segm b1) --> b2 )
let a be finite 0 -based array of the Sorts of Q . K; :: thesis: ( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 11),Q)) . <*a,i*> = a . i & ( for x being Element of Q,K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (11 + 2)),Q)) . <*a*> = card a )
A41: a in ( the Sorts of Q . K) ^omega by AFINSQ_1:def 7;
hereby :: thesis: (Den (( the connectives of S /. (11 + 2)),Q)) . <*a*> = card a
let i be Integer; :: thesis: ( i in dom a implies ( (Den (( the connectives of S /. 11),Q)) . <*a,i*> = a . i & ( for x being Element of Q,K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*a,i,x*> = a +* (i,x) ) ) )
assume A42: i in dom a ; :: thesis: ( (Den (( the connectives of S /. 11),Q)) . <*a,i*> = a . i & ( for x being Element of Q,K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*a,i,x*> = a +* (i,x) ) )
A43: i in INT by INT_1:def 2;
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 11 <= len the connectives of S by XXREAL_0:2;
then 11 in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . 11 = the connectives of S /. 11 & the connectives of S . 11 in the carrier' of S ) by PARTFUN1:def 6, FUNCT_1:102;
then the_arity_of ( the connectives of S /. 11) = <*(the_array_sort_of S), the integer SortSymbol of S*> by A3, A4;
then A44: Args (( the connectives of S /. 11),Q) = product <*( the Sorts of Q . (the_array_sort_of S)),( the Sorts of Q . the integer SortSymbol of S)*> by Th23;
thus (Den (( the connectives of S /. 11),Q)) . <*a,i*> = (Den (( the connectives of S /. 11),A)) . <*a,i*> by A44, A41, A40, A43, A5, A1, FINSEQ_3:124, EQUATION:19
.= a . i by A42, A1, A4, A2 ; :: thesis: for x being Element of Q,K holds (Den (( the connectives of S /. (11 + 1)),Q)) . <*a,i,x*> = a +* (i,x)
let x be Element of Q,K; :: thesis: (Den (( the connectives of S /. (11 + 1)),Q)) . <*a,i,x*> = a +* (i,x)
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 12 <= len the connectives of S by XXREAL_0:2;
then 12 in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . 12 = the connectives of S /. 12 & the connectives of S . 12 in the carrier' of S ) by PARTFUN1:def 6, FUNCT_1:102;
then the_arity_of ( the connectives of S /. 12) = <*(the_array_sort_of S), the integer SortSymbol of S, the integer SortSymbol of S*> by A3, A4;
then A45: Args (( the connectives of S /. 12),Q) = product <*( the Sorts of Q . (the_array_sort_of S)),( the Sorts of Q . the integer SortSymbol of S),( the Sorts of Q . the integer SortSymbol of S)*> by Th24;
thus (Den (( the connectives of S /. (11 + 1)),Q)) . <*a,i,x*> = (Den (( the connectives of S /. (11 + 1)),A)) . <*a,i,x*> by A45, A1, A41, A40, A2, A5, A4, A43, FINSEQ_3:125, EQUATION:19
.= a +* (i,x) by A1, A4, A2, A42 ; :: thesis: verum
end;
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 13 <= len the connectives of S by XXREAL_0:2;
then 13 in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . 13 = the connectives of S /. 13 & the connectives of S . 13 in the carrier' of S ) by PARTFUN1:def 6, FUNCT_1:102;
then the_arity_of ( the connectives of S /. 13) = <*(the_array_sort_of S)*> by A3;
then A46: Args (( the connectives of S /. 13),Q) = product <*( the Sorts of Q . (the_array_sort_of S))*> by Th22;
thus (Den (( the connectives of S /. (11 + 2)),Q)) . <*a*> = (Den (( the connectives of S /. (11 + 2)),A)) . <*a*> by A46, A41, A40, A5, FINSEQ_3:123, EQUATION:19
.= card a by A1, A4, A2 ; :: thesis: verum
end;
let i be Integer; :: thesis: for b1 being Element of the Sorts of Q . K holds
( not 0 <= i or (Den (( the connectives of S /. (11 + 3)),Q)) . <*i,b1*> = (Segm i) --> b1 )
let x be Element of Q,K; :: thesis: ( not 0 <= i or (Den (( the connectives of S /. (11 + 3)),Q)) . <*i,x*> = (Segm i) --> x )
assume A47: i >= 0 ; :: thesis: (Den (( the connectives of S /. (11 + 3)),Q)) . <*i,x*> = (Segm i) --> x
A48: i in INT by INT_1:def 2;
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 14 in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . 14 = the connectives of S /. 14 & the connectives of S . 14 in the carrier' of S ) by PARTFUN1:def 6, FUNCT_1:102;
then the_arity_of ( the connectives of S /. 14) = <* the integer SortSymbol of S,K*> by A3, A2, A4;
then A49: Args (( the connectives of S /. 14),Q) = product <*( the Sorts of Q . the integer SortSymbol of S),( the Sorts of Q . K)*> by Th23;
thus (Den (( the connectives of S /. (11 + 3)),Q)) . <*i,x*> = (Den (( the connectives of S /. (11 + 3)),A)) . <*i,x*> by A49, A48, A1, FINSEQ_3:124, EQUATION:19
.= (Segm i) --> x by A47, A1, A4, A2 ; :: thesis: verum