let S be non empty non void ManySortedSign ; :: thesis: for X being V5() 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 V5() 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 6;
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 4;
then A3: dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;
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:18;
hence dom p = dom (the_arity_of o) by A2, RELAT_1:46; :: 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:22
.= (FreeSort X) . ((the_arity_of o) /. n) by A5, A3, A6, PARTFUN1:def 8
.= FreeSort X,((the_arity_of o) /. n) by Def13 ;
hence p . n in FreeSort X,((the_arity_of o) /. n) by A4, A5, A6, CARD_3:18; :: 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 4;
then A9: dom p = dom ((FreeSort X) * (the_arity_of o)) by A7, RELAT_1:46;
A10: for x being set 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 set ; :: 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 by A9;
FreeSort X,((the_arity_of o) /. n) = (FreeSort X) . ((the_arity_of o) /. n) by Def13
.= (FreeSort X) . ((the_arity_of o) . n) by A7, A9, A11, PARTFUN1:def 8
.= ((FreeSort X) * (the_arity_of o)) . x by A11, FUNCT_1:22 ;
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 6;
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:18; :: thesis: verum