let A be partial non-empty UAStr ; :: thesis: for S being non empty non void ManySortedSign
for G being MSAlgebra over 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 over 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 over 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 15 :: 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 2;
then reconsider SG = the Sorts of G as Function of the carrier of S2,(rng R) by RELSET_1:4;
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;
set h = the Element of product p;
the Element of product p in product r ;
then A5: [ the Element of product p,((Den (o,A)) . the Element of product p)] in Den (o,A) by A4, FUNCT_1:def 2;
then A6: P -index_of [ the Element of product p,((Den (o,A)) . the Element of product p)] in dom P by Def3;
A7: [ the Element of product p,((Den (o,A)) . the Element of product p)] in P . (P -index_of [ the Element of product p,((Den (o,A)) . the Element of product p)]) by A5, Def3;
reconsider Qo = Q . o as Element of rng Q by A2, FUNCT_1:def 3;
A8: dom the Charact of G = the carrier' of S2 by PARTFUN1:def 2;
then A9: dom P = Qo by RELAT_1:62;
reconsider s = P -index_of [ the Element of product p,((Den (o,A)) . the Element of product p)] as Element of Qo by A6, A8, RELAT_1:62;
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 Th8;
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:13
.= product q by FINSEQ_2:def 5 ;
A11: product q in Q ;
A12: product p in Q ;
P . s = the Charact of G . s by A9, FUNCT_1:47;
then the Element of product p in dom (Den (s,G)) by A7, XTUPLE_0:def 12;
hence the Sorts of G * (the_arity_of s) = r by A10, A11, A12, Th2, Lm3; :: thesis: s in Q . o
thus s in Q . o ; :: thesis: verum