let Q be non-empty MSSubAlgebra of A; :: thesis:
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:
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 ;

suppose len a = 0 ; :: thesis:

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:

end;

suppose A8: len a <> 0 ; :: thesis:

deffunc H₁( array, Integer, set ) -> set = S +* (A,c₃);
deffunc H₂( 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 H₁(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
H₂(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) = H₁(f . i,i,H₂(i)) ) ) from AOFA_A01:sch 1(A9, A10, A11);
reconsider f = f as Function-yielding FinSequence of INT ^omega ;
defpred S₁[ 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: S₁[ 0 ] ;

A14: now :: thesis:

let i be Nat; :: thesis:
assume A15: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

proof

assume A16: i + 1 <= len a ; :: thesis:

per cases ;

suppose A17: i = 0 ; :: thesis:

thus ( i + 1 <> 0 implies len (f . (i + 1)) = len a ) by A12, A16, A17; :: thesis:
let k be Nat; :: thesis:
assume k < i + 1 ; :: thesis:
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:

end;

suppose A19: i > 0 ; :: thesis:

then A20: ( i >= 0 + 1 & i < len a ) by A16, NAT_1:13;
then A21: f . (i + 1) = H₁(f . i,i,H₂(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:
let k be Nat; :: thesis:
assume k < i + 1 ; :: thesis:
then A22: ( k <= i & k < len a ) by A16, XXREAL_0:2, NAT_1:13;

per cases by A22, XXREAL_0:1;

suppose k = i ; :: thesis:

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:

end;

suppose A23: k < i ; :: thesis:

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:

end;

A25: for i being Nat holds S₁[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 S₂[ Nat] means ( 1 <= S & S <= len a implies f . S in the Sorts of Q . (the_array_sort_of S) );
A27: S₂[ 0 ] ;

A28: now :: thesis:

let i be Nat; :: thesis:
assume A29: S₂[i] ; :: thesis:
thus S₂[i + 1] :: thesis:

proof

assume A30: ( 1 <= i + 1 & i + 1 <= len a ) ; :: thesis:
then A31: i < len a by NAT_1:13;

per cases by NAT_1:14;

suppose A32: i >= 1 ; :: thesis:

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 = H₂(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) = H₁(f . i,i,H₂(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:

end;

suppose A36: i = 0 ; :: thesis:

end;

A39: for i being Nat holds S₂[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:

end;

take J ; :: according to AOFA_A00:def 51 :: thesis:
take K ; :: thesis:
thus K = 1 by A2; :: thesis:
thus the connectives of S . 11 is_of_type <*J,1*>,K by A2; :: thesis:
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:
thus A40: ( the Sorts of Q . K) ^omega c= the Sorts of Q . J by A5, A6, A1, A4, A2; :: thesis:
thus the Sorts of Q . 1 = INT by AOFA_A00:55, A4; :: thesis:

hereby :: thesis:

let a be finite 0 -based array of the Sorts of Q . K; :: thesis:
A41: a in ( the Sorts of Q . K) ^omega by AFINSQ_1:def 7;

hereby :: thesis:

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:

end;