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

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

end;

assume A5: ( 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: p in (((ParsedTerms X) # ) * the Arity of S) . o
the Arity of S . o = the_arity_of o by MSUALG_1:def 6;
then A6: (((ParsedTerms X) # ) * the Arity of S) . o = product ((ParsedTerms X) * (the_arity_of o)) by MSAFREE:1;
A7: dom p = dom ((ParsedTerms X) * (the_arity_of o)) by A5, PBOOLE:def 3;
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 A8: 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 A5, A7, A8, PARTFUN1:def 8
.= ((ParsedTerms X) * (the_arity_of o)) . x by A8, FUNCT_1:22 ;
hence p . x in ((ParsedTerms X) * (the_arity_of o)) . x by A5, A7, A8; :: thesis: verum

end;

hence p in (((ParsedTerms X) # ) * the Arity of S) . o by A6, A7, CARD_3:18; :: thesis: verum