let A be partial non-empty UAStr ; :: thesis: for S being non empty non void ManySortedSign
for G being MSAlgebra of S
for Q being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den o,A) holds
ex s being OperSymbol of S st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let S2 be non empty non void ManySortedSign ; :: thesis: for G being MSAlgebra of S2
for Q being IndexedPartition of the carrier' of S2 st A can_be_characterized_by S2,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den o,A) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let G be MSAlgebra of S2; :: thesis: for Q being IndexedPartition of the carrier' of S2 st A can_be_characterized_by S2,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den o,A) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let Q be IndexedPartition of the carrier' of S2; :: thesis: ( A can_be_characterized_by S2,G,Q implies for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den o,A) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o ) )
assume that
A1: ( the Sorts of G is IndexedPartition of A & dom Q = dom the charact of A ) and
A2: for o being OperSymbol of A holds the Charact of G | (Q . o) is IndexedPartition of Den o,A ; :: according to PUA2MSS1:def 16 :: thesis: for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den o,A) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
reconsider R = the Sorts of G as IndexedPartition of A by A1;
dom R = the carrier of S2 by PARTFUN1:def 4;
then reconsider SG = the Sorts of G as Function of the carrier of S2,(rng R) by RELSET_1:11;
let o be OperSymbol of A; :: thesis: for r being FinSequence of rng the Sorts of G st product r c= dom (Den o,A) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let r be FinSequence of rng the Sorts of G; :: thesis: ( product r c= dom (Den o,A) implies ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o ) )
reconsider p = r as Element of (rng R) * by FINSEQ_1:def 11;
assume A3: product r c= dom (Den o,A) ; :: thesis: ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
reconsider P = the Charact of G | (Q . o) as IndexedPartition of Den o,A by A2;
consider h being Element of product p;
h in product r ;
then [h,((Den o,A) . h)] in Den o,A by A3, FUNCT_1:def 4;
then A4: ( P -index_of [h,((Den o,A) . h)] in dom P & [h,((Den o,A) . h)] in P . (P -index_of [h,((Den o,A) . h)]) ) by Def4;
reconsider Qo = Q . o as Element of rng Q by A1, FUNCT_1:def 5;
A5: dom the Charact of G = the carrier' of S2 by PARTFUN1:def 4;
then A6: dom P = Qo by RELAT_1:91;
reconsider s = P -index_of [h,((Den o,A) . h)] as Element of Qo by A4, A5, RELAT_1:91;
reconsider q = SG * (the_arity_of s) as FinSequence of rng R by Lm2;
reconsider q = q as Element of (rng R) * by FINSEQ_1:def 11;
reconsider Q = { (product t) where t is Element of (rng R) * : verum } as a_partition of the carrier of A * by Th9;
take s ; :: thesis: ( the Sorts of G * (the_arity_of s) = r & s in Q . o )
dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
then A7: Args s,G = (the Sorts of G # ) . (the Arity of S2 . s) by FUNCT_1:23
.= product q by PBOOLE:def 19 ;
A8: ( product q in Q & product p in Q ) ;
P . s = the Charact of G . s by A6, FUNCT_1:70;
then h in dom (Den s,G) by A4, RELAT_1:def 4;
hence the Sorts of G * (the_arity_of s) = r by A7, A8, Th2, Th3; :: thesis: s in Q . o
thus s in Q . o ; :: thesis: verum