let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; for I being integer SortSymbol of S
for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S holds
( the Sorts of A . (the_array_sort_of S) = INT ^omega & ( for i, j being Element of A,I st i is non negative Integer holds
init.array (i,j) = (Segm i) --> j ) & ( for a being Element of the Sorts of A . (the_array_sort_of S) holds
( length (a,I) = card a & ( for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) ) ) )
let I be integer SortSymbol of S; for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S holds
( the Sorts of A . (the_array_sort_of S) = INT ^omega & ( for i, j being Element of A,I st i is non negative Integer holds
init.array (i,j) = (Segm i) --> j ) & ( for a being Element of the Sorts of A . (the_array_sort_of S) holds
( length (a,I) = card a & ( for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) ) ) )
let A be non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S; ( the Sorts of A . (the_array_sort_of S) = INT ^omega & ( for i, j being Element of A,I st i is non negative Integer holds
init.array (i,j) = (Segm i) --> j ) & ( for a being Element of the Sorts of A . (the_array_sort_of S) holds
( length (a,I) = card a & ( for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) ) ) )
consider J, K being Element of S such that
A1:
( 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;
thus
the Sorts of A . (the_array_sort_of S) = INT ^omega
by A1, Th71; ( ( for i, j being Element of A,I st i is non negative Integer holds
init.array (i,j) = (Segm i) --> j ) & ( for a being Element of the Sorts of A . (the_array_sort_of S) holds
( length (a,I) = card a & ( for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) ) ) )
11 + 3 <= len the connectives of S
by AOFA_A00:def 51;
then
( 11 <= len the connectives of S & 12 <= len the connectives of S & 13 <= len the connectives of S & 14 <= len the connectives of S )
by XXREAL_0:2;
then
( 11 in dom the connectives of S & 12 in dom the connectives of S & 13 in dom the connectives of S & 14 in dom the connectives of S )
by FINSEQ_3:25;
then A2:
( the connectives of S . 11 in the carrier' of S & the connectives of S . 12 in the carrier' of S & the connectives of S . 13 in the carrier' of S & the connectives of S . 14 in the carrier' of S & the connectives of S . 11 = the connectives of S /. 11 & the connectives of S . 12 = the connectives of S /. 12 & the connectives of S . 13 = the connectives of S /. 13 & the connectives of S . 14 = the connectives of S /. 14 )
by FUNCT_1:102, PARTFUN1:def 6;
A3:
I = 1
by AOFA_A00:def 40;
hereby for a being Element of the Sorts of A . (the_array_sort_of S) holds
( length (a,I) = card a & ( for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) )
let i,
j be
Element of
A,
I;
( i is non negative Integer implies init.array (i,j) = (Segm i) --> j )reconsider ii =
i as
Integer by A3;
assume
i is non
negative Integer
;
init.array (i,j) = (Segm i) --> jthen A4:
(
ii >= 0 &
I = K )
by A1, AOFA_A00:def 40;
thus init.array (
i,
j) =
(Den (( the connectives of S /. 14),A)) . <*ii,j*>
by A2, SUBSET_1:def 8
.=
(Segm i) --> j
by A1, A4
;
verum
end;
let a be Element of the Sorts of A . (the_array_sort_of S); ( length (a,I) = card a & ( for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) )
J = the_array_sort_of S
by A1, Th71;
then reconsider b = a as XFinSequence of INT by A1;
thus length (a,I) =
(Den (( the connectives of S /. 13),A)) . <*b*>
by A2, SUBSET_1:def 8
.=
card a
by A1
; for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) )
let i be Element of A,I; for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) )
let f be Function; ( f = a & i in dom f implies ( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) )
assume A5:
( f = a & i in dom f )
; ( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) )
thus a . i =
(Den (( the connectives of S /. 11),A)) . <*a,i*>
by A2, SUBSET_1:def 8
.=
b . i
by A1, A5, A3
.=
f . i
by A5
; for x being Element of A,I holds (a,i) <- x = f +* (i,x)
let x be Element of A,I; (a,i) <- x = f +* (i,x)
thus (a,i) <- x =
(Den (( the connectives of S /. 12),A)) . <*b,i,x*>
by A2, SUBSET_1:def 8
.=
f +* (i,x)
by A1, A3, A5
; verum