let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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)) ) ) ) :: thesis: ( 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 )

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)) ; :: thesis: 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

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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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)) ) ) ) :: thesis: ( 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

assume that
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 ; :: thesis: ( 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; :: thesis: for n being Nat st n in dom p holds

p . n in FreeSort (X,((the_arity_of o) /. n))

let n be Nat; :: thesis: ( n in dom p implies p . n in FreeSort (X,((the_arity_of o) /. n)) )

assume A6: n in dom p ; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: ( 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; :: thesis: for n being Nat st n in dom p holds

p . n in FreeSort (X,((the_arity_of o) /. n))

let n be Nat; :: thesis: ( n in dom p implies p . n in FreeSort (X,((the_arity_of o) /. n)) )

assume A6: n in dom p ; :: thesis: 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; :: thesis: verum

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)) ; :: thesis: 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

proof

the Arity of S . o = the_arity_of o
by MSUALG_1:def 1;
let x be object ; :: thesis: ( x in dom ((FreeSort X) * (the_arity_of o)) implies p . x in ((FreeSort X) * (the_arity_of o)) . x )

assume A11: x in dom ((FreeSort X) * (the_arity_of o)) ; :: thesis: p . x in ((FreeSort X) * (the_arity_of o)) . x

then reconsider n = x as Nat ;

FreeSort (X,((the_arity_of o) /. n)) = (FreeSort X) . ((the_arity_of o) /. n) by Def11

.= (FreeSort X) . ((the_arity_of o) . n) by A7, A9, A11, PARTFUN1:def 6

.= ((FreeSort X) * (the_arity_of o)) . x by A11, FUNCT_1:12 ;

hence p . x in ((FreeSort X) * (the_arity_of o)) . x by A8, A9, A11; :: thesis: verum

end;assume A11: x in dom ((FreeSort X) * (the_arity_of o)) ; :: thesis: p . x in ((FreeSort X) * (the_arity_of o)) . x

then reconsider n = x as Nat ;

FreeSort (X,((the_arity_of o) /. n)) = (FreeSort X) . ((the_arity_of o) /. n) by Def11

.= (FreeSort X) . ((the_arity_of o) . n) by A7, A9, A11, PARTFUN1:def 6

.= ((FreeSort X) * (the_arity_of o)) . x by A11, FUNCT_1:12 ;

hence p . x in ((FreeSort X) * (the_arity_of o)) . x by A8, A9, A11; :: thesis: verum

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; :: thesis: verum