let n, m be Nat; :: thesis: for s, r being set st n >= 1 & m >= 1 holds
for B being non empty non void m -connectives BoolSignature
for A1 being non-empty MSAlgebra over B
for C being non empty non void ConnectivesSignature st C is n,s,r -array holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
let s, r be set ; :: thesis: ( n >= 1 & m >= 1 implies for B being non empty non void m -connectives BoolSignature
for A1 being non-empty MSAlgebra over B
for C being non empty non void ConnectivesSignature st C is n,s,r -array holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array )
assume A1: ( n >= 1 & m >= 1 ) ; :: thesis: for B being non empty non void m -connectives BoolSignature
for A1 being non-empty MSAlgebra over B
for C being non empty non void ConnectivesSignature st C is n,s,r -array holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
let B be non empty non void m -connectives BoolSignature ; :: thesis: for A1 being non-empty MSAlgebra over B
for C being non empty non void ConnectivesSignature st C is n,s,r -array holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
let A1 be non-empty MSAlgebra over B; :: thesis: for C being non empty non void ConnectivesSignature st C is n,s,r -array holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
let C be non empty non void ConnectivesSignature ; :: thesis: ( C is n,s,r -array implies for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array )
assume A2: C is n,s,r -array ; :: thesis: for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
then A3: ( len the connectives of C >= n + 3 & ex J, K, L being Element of C st
( L = s & K = r & J <> L & J <> K & the connectives of C . n is_of_type <*J,K*>,L & the connectives of C . (n + 1) is_of_type <*J,K,L*>,J & the connectives of C . (n + 2) is_of_type <*J*>,K & the connectives of C . (n + 3) is_of_type <*K,L*>,J ) ) ;
let A2 be non-empty MSAlgebra over C; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array implies for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array )
assume A4: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: ( not A2 is n,s,r -array or for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array )
given J, K being Element of C such that A5: ( K = s & the connectives of C . n is_of_type <*J,r*>,K & the Sorts of A2 . J = ( the Sorts of A2 . K) ^omega & the Sorts of A2 . r = INT & ( for a being finite 0 -based array of the Sorts of A2 . K holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of C /. n),A2)) . <*a,i*> = a . i & ( for x being Element of A2,K holds (Den (( the connectives of C /. (n + 1)),A2)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of C /. (n + 2)),A2)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A2,K st i >= 0 holds
(Den (( the connectives of C /. (n + 3)),A2)) . <*i,x*> = (Segm i) --> x ) ) ; :: according to AOFA_A00:def 51 :: thesis: for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
let S be non empty non void BoolSignature ; :: thesis: ( BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C implies for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array )
assume A6: BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C ; :: thesis: for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
set k = K;
the carrier of S = the carrier of B \/ the carrier of C by A6, Th51;
then reconsider J = J, K = K as Element of S by XBOOLE_0:def 3;
reconsider k0 = K as Element of (B +* C) by A6;
let A be non-empty MSAlgebra over S; :: thesis: ( A = (B,A1) +* A2 implies A is m + n,s,r -array )
assume A7: A = (B,A1) +* A2 ; :: thesis: A is m + n,s,r -array
take J ; :: according to AOFA_A00:def 51 :: thesis: ex K being Element of S st
( K = s & the connectives of S . (m + n) is_of_type <*J,r*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . r = 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 /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. ((m + n) + 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 /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
take K ; :: thesis: ( K = s & the connectives of S . (m + n) is_of_type <*J,r*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . r = 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 /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. ((m + n) + 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 /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
thus K = s by A5; :: thesis: ( the connectives of S . (m + n) is_of_type <*J,r*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . r = 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 /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. ((m + n) + 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 /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
A8: len the connectives of B = m by Def29;
A9: the connectives of S = the connectives of B ^ the connectives of C by A6, Def52;
A10: dom the Sorts of A2 = the carrier of C by PARTFUN1:def 2;
A11: r in dom the Sorts of A2 by A5, FUNCT_1:def 2;
reconsider R = r as Element of C by A10, A5, FUNCT_1:def 2;
A12: the Arity of S = the Arity of B +* the Arity of C by A6, Th51;
n > 0 by A1;
then A13: B +* C is m + n,s,r -array by A2, Th53;
then A14: len the connectives of (B +* C) >= (m + n) + 3 ;
consider J0, K0, L0 being Element of (B +* C) such that
A15: ( L0 = s & K0 = r & J0 <> L0 & J0 <> K0 & the connectives of (B +* C) . (m + n) is_of_type <*J0,K0*>,L0 & the connectives of (B +* C) . ((m + n) + 1) is_of_type <*J0,K0,L0*>,J0 ) and
( the connectives of (B +* C) . ((m + n) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((m + n) + 3) is_of_type <*K0,L0*>,J0 ) by A13;
A16: ( the Sorts of A = the Sorts of A1 +* the Sorts of A2 & the Charact of A = the Charact of A1 +* the Charact of A2 ) by A4, A7, CIRCCOMB:def 4;
( m + n <= (m + n) + 3 & n <= n + 3 ) by NAT_1:11;
then ( 1 <= m + n & m + n <= len the connectives of S & 1 <= n & n <= len the connectives of C ) by A1, A6, A3, A14, NAT_1:12, XXREAL_0:2;
then A17: ( m + n in dom the connectives of S & n in dom the connectives of C & dom the Sorts of A2 = the carrier of C & dom the Arity of C = the carrier' of C ) by PARTFUN1:def 2, FINSEQ_3:25;
then A18: ( the connectives of S /. (m + n) = the connectives of S . (m + n) & the connectives of C /. n = the connectives of C . n & the connectives of C . n = the connectives of S . (m + n) ) by A9, A8, PARTFUN1:def 6, FINSEQ_1:def 7;
the Arity of S . ( the connectives of S . (m + n)) = the Arity of C . ( the connectives of C . n) by A12, A18, A17, FUNCT_4:13;
then <*J0,r*> = the Arity of C . ( the connectives of C . n) by A6, A15
.= <*J,r*> by A5 ;
then J0 = <*J,r*> . 1
.= J ;
then ( the connectives of (B +* C) . (m + n) is_of_type <*J,r*>,k0 & ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C) #) ) by A6, A15, A5;
hence the connectives of S . (m + n) is_of_type <*J,r*>,K by A6; :: thesis: ( the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . r = 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 /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. ((m + n) + 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 /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x ) )
( the Sorts of A . K = the Sorts of A2 . K & the Sorts of A . r = the Sorts of A2 . r & the Sorts of A . J = the Sorts of A2 . J ) by A10, A11, A16, FUNCT_4:13;
hence ( the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . r = INT ) by A5; :: thesis: ( ( 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 /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. ((m + n) + 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 /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x ) )

hereby :: thesis: for i being Integer
for x being Element of A,K st i >= 0 holds
(Den (( the connectives of S /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x

let a be finite 0 -based array of the Sorts of A . K; :: thesis: ( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. ((m + n) + 2)),A)) . <*a*> = card a )

hereby :: thesis: (Den (( the connectives of S /. ((m + n) + 2)),A)) . <*a*> = card a

let i be Integer; :: thesis: ( i in dom a implies ( (Den (( the connectives of S /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) )
assume A19: i in dom a ; :: thesis: ( (Den (( the connectives of S /. (m + n)),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) ) )
( the connectives of C . n in the carrier' of C & dom the Charact of A2 = the carrier' of C & dom the Sorts of A2 = the carrier of C ) by A18, PARTFUN1:def 2;
then ( the Charact of A2 . ( the connectives of C /. n) = the Charact of A . ( the connectives of S /. (m + n)) & the Sorts of A2 . s = the Sorts of A . s ) by A5, A16, A18, FUNCT_4:13;
hence (Den (( the connectives of S /. (m + n)),A)) . <*a,i*> = a . i by A19, A5; :: thesis: for x being Element of A,K holds (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x)
let x be Element of A,K; :: thesis: (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x)
( (m + n) + 1 <= ((m + n) + 1) + 2 & n + 1 <= (n + 1) + 2 ) by NAT_1:11;
then ( 1 <= (m + n) + 1 & (m + n) + 1 <= len the connectives of S & 1 <= n + 1 & n + 1 <= len the connectives of C ) by A6, A3, A14, NAT_1:12, XXREAL_0:2;
then A20: ( (m + n) + 1 in dom the connectives of S & n + 1 in dom the connectives of C & dom the Sorts of A2 = the carrier of C ) by PARTFUN1:def 2, FINSEQ_3:25;
A21: ( the connectives of S /. ((m + n) + 1) = the connectives of S . ((m + n) + 1) & the connectives of C /. (n + 1) = the connectives of C . (n + 1) & the connectives of C . (n + 1) = the connectives of S . (m + (n + 1)) ) by A9, A8, A20, PARTFUN1:def 6, FINSEQ_1:def 7;
then ( the connectives of C . (n + 1) in the carrier' of C & dom the Charact of A2 = the carrier' of C & m + (n + 1) = (m + n) + 1 & dom the Sorts of A2 = the carrier of C ) by PARTFUN1:def 2;
then ( the Charact of A2 . ( the connectives of C /. (n + 1)) = the Charact of A . ( the connectives of S /. ((m + n) + 1)) & the Sorts of A2 . K = the Sorts of A . k0 ) by A16, A21, FUNCT_4:13;
hence (Den (( the connectives of S /. ((m + n) + 1)),A)) . <*a,i,x*> = a +* (i,x) by A5, A19; :: thesis: verum

end;

( (m + n) + 2 <= ((m + n) + 2) + 1 & (m + n) + 3 <= len the connectives of S & (n + 2) + 1 >= n + 2 & n + 3 <= len the connectives of C ) by A13, A2, A6, NAT_1:11;
then ( 1 <= (m + n) + 2 & (m + n) + 2 <= len the connectives of S & 1 <= n + 2 & n + 2 <= len the connectives of C ) by XXREAL_0:2, NAT_1:12;
then A22: ( (m + n) + 2 in dom the connectives of S & n + 2 in dom the connectives of C & dom the Sorts of A2 = the carrier of C ) by PARTFUN1:def 2, FINSEQ_3:25;
A23: ( the connectives of S /. ((m + n) + 2) = the connectives of S . ((m + n) + 2) & the connectives of C /. (n + 2) = the connectives of C . (n + 2) & the connectives of C . (n + 2) = the connectives of S . (m + (n + 2)) ) by A9, A8, A22, PARTFUN1:def 6, FINSEQ_1:def 7;
then ( the connectives of C . (n + 2) in the carrier' of C & dom the Charact of A2 = the carrier' of C & m + (n + 2) = (m + n) + 2 & dom the Sorts of A2 = the carrier of C ) by PARTFUN1:def 2;
then ( the Charact of A2 . ( the connectives of C /. (n + 2)) = the Charact of A . ( the connectives of S /. ((m + n) + 2)) & the Sorts of A2 . K = the Sorts of A . k0 ) by A16, A23, FUNCT_4:13;
hence (Den (( the connectives of S /. ((m + n) + 2)),A)) . <*a*> = card a by A5; :: thesis: verum

end;

let i be Integer; :: thesis: for x being Element of A,K st i >= 0 holds
(Den (( the connectives of S /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x
let x be Element of A,K; :: thesis: ( i >= 0 implies (Den (( the connectives of S /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x )
assume A24: i >= 0 ; :: thesis: (Den (( the connectives of S /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x
( 1 <= (m + n) + 3 & (m + n) + 3 <= len the connectives of S & 1 <= n + 3 & n + 3 <= len the connectives of C ) by A2, A6, A13, NAT_1:12;
then A25: ( (m + n) + 3 in dom the connectives of S & n + 3 in dom the connectives of C & dom the Sorts of A2 = the carrier of C ) by PARTFUN1:def 2, FINSEQ_3:25;
A26: ( the connectives of S /. ((m + n) + 3) = the connectives of S . ((m + n) + 3) & the connectives of C /. (n + 3) = the connectives of C . (n + 3) & the connectives of C . (n + 3) = the connectives of S . (m + (n + 3)) ) by A9, A8, A25, PARTFUN1:def 6, FINSEQ_1:def 7;
then ( the connectives of C . (n + 3) in the carrier' of C & dom the Charact of A2 = the carrier' of C & m + (n + 3) = (m + n) + 3 & dom the Sorts of A2 = the carrier of C ) by PARTFUN1:def 2;
then ( the Charact of A2 . ( the connectives of C /. (n + 3)) = the Charact of A . ( the connectives of S /. ((m + n) + 3)) & the Sorts of A2 . K = the Sorts of A . k0 ) by A16, A26, FUNCT_4:13;
hence (Den (( the connectives of S /. ((m + n) + 3)),A)) . <*i,x*> = (Segm i) --> x by A5, A24; :: thesis: verum