let S be OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConOSA X) holds
( p in (((ParsedTerms 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 ParsedTerms (X,((the_arity_of o) /. n)) ) ) )
let X be non-empty ManySortedSet of S; :: thesis: for o being OperSymbol of S
for p being FinSequence of TS (DTConOSA X) holds
( p in (((ParsedTerms 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 ParsedTerms (X,((the_arity_of o) /. n)) ) ) )
let o be OperSymbol of S; :: thesis: for p being FinSequence of TS (DTConOSA X) holds
( p in (((ParsedTerms 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 ParsedTerms (X,((the_arity_of o) /. n)) ) ) )
let p be FinSequence of TS (DTConOSA X); :: thesis: ( p in (((ParsedTerms 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 ParsedTerms (X,((the_arity_of o) /. n)) ) ) )
set AR = the Arity of S;
set ar = the_arity_of o;
thus ( p in (((ParsedTerms 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 ParsedTerms (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 ParsedTerms (X,((the_arity_of o) /. n)) ) implies p in (((ParsedTerms X) #) * the Arity of S) . o )

proof

A1: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
assume p in (((ParsedTerms 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 ParsedTerms (X,((the_arity_of o) /. n)) ) )
then A2: p in product ((ParsedTerms X) * (the_arity_of o)) by A1, MSAFREE:1;
then A3: dom p = dom ((ParsedTerms X) * (the_arity_of o)) by CARD_3:9;
hence dom p = dom (the_arity_of o) by PARTFUN1:def 2; :: thesis: for n being Nat st n in dom p holds
p . n in ParsedTerms (X,((the_arity_of o) /. n))
A4: dom ((ParsedTerms X) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
let n be Nat; :: thesis: ( n in dom p implies p . n in ParsedTerms (X,((the_arity_of o) /. n)) )
assume A5: n in dom p ; :: thesis: p . n in ParsedTerms (X,((the_arity_of o) /. n))
then ((ParsedTerms X) * (the_arity_of o)) . n = (ParsedTerms X) . ((the_arity_of o) . n) by A3, FUNCT_1:12
.= (ParsedTerms X) . ((the_arity_of o) /. n) by A3, A4, A5, PARTFUN1:def 6
.= ParsedTerms (X,((the_arity_of o) /. n)) by Def8 ;
hence p . n in ParsedTerms (X,((the_arity_of o) /. n)) by A2, A3, A5, CARD_3:9; :: thesis: verum

end;

assume that
A6: dom p = dom (the_arity_of o) and
A7: for n being Nat st n in dom p holds
p . n in ParsedTerms (X,((the_arity_of o) /. n)) ; :: thesis: p in (((ParsedTerms X) #) * the Arity of S) . o
A8: dom p = dom ((ParsedTerms X) * (the_arity_of o)) by A6, PARTFUN1:def 2;
A9: for x being object st x in dom ((ParsedTerms X) * (the_arity_of o)) holds
p . x in ((ParsedTerms X) * (the_arity_of o)) . x

proof

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

end;

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