let S be non empty non void ManySortedSign ; 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; 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; 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); ( 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)) ) ) )
( 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 1;
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 2;
then A3:
dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27;
assume
p in (((FreeSort 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 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:9;
hence
dom p = dom (the_arity_of o)
by A2, RELAT_1:27;
for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n))
let n be
Nat;
( n in dom p implies p . n in FreeSort (X,((the_arity_of o) /. n)) )
assume A6:
n in dom p
;
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:12
.=
(FreeSort X) . ((the_arity_of o) /. n)
by A5, A3, A6, PARTFUN1:def 6
.=
FreeSort (
X,
((the_arity_of o) /. n))
by Def11
;
hence
p . n in FreeSort (
X,
((the_arity_of o) /. n))
by A4, A5, A6, CARD_3:9;
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))
; 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 2;
then A9:
dom p = dom ((FreeSort X) * (the_arity_of o))
by A7, RELAT_1:27;
A10:
for x being object st x in dom ((FreeSort X) * (the_arity_of o)) holds
p . x in ((FreeSort X) * (the_arity_of o)) . x
the Arity of S . o = the_arity_of o
by MSUALG_1:def 1;
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:9; verum