let S be OrderSortedSign; :: thesis: for X being V5() 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 V5() 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 6;
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:18;
hence dom p = dom (the_arity_of o) by PARTFUN1:def 4; :: 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 4;
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:22
.= (ParsedTerms X) . ((the_arity_of o) /. n) by A3, A4, A5, PARTFUN1:def 8
.= 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:18; :: 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 4;
A9: for x being set 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 set ; :: 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 8
.= ((ParsedTerms X) * (the_arity_of o)) . x by A10, FUNCT_1:22 ;
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 6;
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:18; :: thesis: verum