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 and
A2: dom Q = dom the charact of A and
A3: 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 A4: 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 A3;
consider h being Element of product p;
h in product r ;
then A5: [h,((Den (o,A)) . h)] in Den (o,A) by A4, FUNCT_1:def 4;
then A6: P -index_of [h,((Den (o,A)) . h)] in dom P by Def4;
A7: [h,((Den (o,A)) . h)] in P . (P -index_of [h,((Den (o,A)) . h)]) by A5, Def4;
reconsider Qo = Q . o as Element of rng Q by A2, FUNCT_1:def 5;
A8: dom the Charact of G = the carrier' of S2 by PARTFUN1:def 4;
then A9: dom P = Qo by RELAT_1:91;
reconsider s = P -index_of [h,((Den (o,A)) . h)] as Element of Qo by A6, A8, 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 A10: Args (s,G) = ( the Sorts of G #) . ( the Arity of S2 . s) by FUNCT_1:23
.= product q by PBOOLE:def 19 ;
A11: product q in Q ;
A12: product p in Q ;
P . s = the Charact of G . s by A9, FUNCT_1:70;
then h in dom (Den (s,G)) by A7, RELAT_1:def 4;
hence the Sorts of G * (the_arity_of s) = r by A10, A11, A12, Th2, Th3; :: thesis: s in Q . o
thus s in Q . o ; :: thesis: verum