let S be OrderSortedSign; for X being V2() 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 V2() 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 o be 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 p be FinSequence of TS (DTConOSA X); ( 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)) ) ) )
( 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
;
( 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;
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;
( n in dom p implies p . n in ParsedTerms (X,((the_arity_of o) /. n)) )
assume A5:
n in dom p
;
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;
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))
; 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
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; verum