let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
let o be OperSymbol of S; :: thesis: for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
let p be FinSequence of TS (DTConMSA X); :: thesis: ( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
set AR = the Arity of S;
set cr = the carrier of S;
set ar = the_arity_of o;
thus ( p in (((FreeSort X) #) * the Arity of S) . o implies ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) ) :: thesis: ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) implies p in (((FreeSort X) #) * the Arity of S) . o )

proof

A1: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
A2: ( rng (the_arity_of o) c= the carrier of S & dom (FreeSort X) = the carrier of S ) by FINSEQ_1:def 4, PARTFUN1:def 2;
then A3: dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
assume p in (((FreeSort X) #) * the Arity of S) . o ; :: thesis: ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) )
then A4: p in product ((FreeSort X) * (the_arity_of o)) by A1, Th1;
then A5: dom p = dom ((FreeSort X) * (the_arity_of o)) by CARD_3:9;
hence dom p = dom (the_arity_of o) by A2, RELAT_1:27; :: thesis: for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n))
let n be Nat; :: thesis: ( n in dom p implies p . n in FreeSort (X,((the_arity_of o) /. n)) )
assume A6: n in dom p ; :: thesis: p . n in FreeSort (X,((the_arity_of o) /. n))
then ((FreeSort X) * (the_arity_of o)) . n = (FreeSort X) . ((the_arity_of o) . n) by A5, FUNCT_1:12
.= (FreeSort X) . ((the_arity_of o) /. n) by A5, A3, A6, PARTFUN1:def 6
.= FreeSort (X,((the_arity_of o) /. n)) by Def11 ;
hence p . n in FreeSort (X,((the_arity_of o) /. n)) by A4, A5, A6, CARD_3:9; :: thesis: verum

end;

assume that
A7: dom p = dom (the_arity_of o) and
A8: for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ; :: thesis: p in (((FreeSort X) #) * the Arity of S) . o
( rng (the_arity_of o) c= the carrier of S & dom (FreeSort X) = the carrier of S ) by FINSEQ_1:def 4, PARTFUN1:def 2;
then A9: dom p = dom ((FreeSort X) * (the_arity_of o)) by A7, RELAT_1:27;
A10: for x being object st x in dom ((FreeSort X) * (the_arity_of o)) holds
p . x in ((FreeSort X) * (the_arity_of o)) . x

proof

let x be object ; :: thesis: ( x in dom ((FreeSort X) * (the_arity_of o)) implies p . x in ((FreeSort X) * (the_arity_of o)) . x )
assume A11: x in dom ((FreeSort X) * (the_arity_of o)) ; :: thesis: p . x in ((FreeSort X) * (the_arity_of o)) . x
then reconsider n = x as Nat ;
FreeSort (X,((the_arity_of o) /. n)) = (FreeSort X) . ((the_arity_of o) /. n) by Def11
.= (FreeSort X) . ((the_arity_of o) . n) by A7, A9, A11, PARTFUN1:def 6
.= ((FreeSort X) * (the_arity_of o)) . x by A11, FUNCT_1:12 ;
hence p . x in ((FreeSort X) * (the_arity_of o)) . x by A8, A9, A11; :: thesis: verum

end;

the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
then (((FreeSort X) #) * the Arity of S) . o = product ((FreeSort X) * (the_arity_of o)) by Th1;
hence p in (((FreeSort X) #) * the Arity of S) . o by A9, A10, CARD_3:9; :: thesis: verum