let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for I being integer SortSymbol of S
for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S
for a, b being Element of A,I st a = 0 holds
init.array (a,b) = {}
let I be integer SortSymbol of S; :: thesis: for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S
for a, b being Element of A,I st a = 0 holds
init.array (a,b) = {}
let A be non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S; :: thesis: for a, b being Element of A,I st a = 0 holds
init.array (a,b) = {}
let a, b be Element of A,I; :: thesis: ( a = 0 implies init.array (a,b) = {} )
assume A1: a = 0 ; :: thesis: init.array (a,b) = {}
set o = the connectives of S . 14;
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;
A3: I = 1 by AOFA_A00:def 40;
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 FUNCT_1:102, PARTFUN1:def 6;
hence init.array (a,b) = (Den (( the connectives of S /. 14),A)) . <*a,b*> by SUBSET_1:def 8
.= (Segm 0) --> b by A1, A2, A3
.= {} ;
:: thesis: verum