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 x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S

for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

let o be OperSymbol of S; :: thesis: for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

let x be set ; :: thesis: ( x in (((FreeSort X) #) * the Arity of S) . o implies x is FinSequence of TS (DTConMSA X) )

set D = DTConMSA X;

set ar = the_arity_of o;

set cr = the carrier of S;

A1: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;

( 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 A2: dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

assume x in (((FreeSort X) #) * the Arity of S) . o ; :: thesis: x is FinSequence of TS (DTConMSA X)

then x in product ((FreeSort X) * (the_arity_of o)) by A1, Th1;

then consider f being Function such that

A3: x = f and

A4: dom f = dom ((FreeSort X) * (the_arity_of o)) and

A5: for y being object st y in dom ((FreeSort X) * (the_arity_of o)) holds

f . y in ((FreeSort X) * (the_arity_of o)) . y by CARD_3:def 5;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then reconsider f = f as FinSequence by A4, A2, FINSEQ_1:def 2;

rng f c= TS (DTConMSA X)

f = x by A3;

hence x is FinSequence of TS (DTConMSA X) ; :: thesis: verum

for o being OperSymbol of S

for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S

for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

let o be OperSymbol of S; :: thesis: for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConMSA X)

let x be set ; :: thesis: ( x in (((FreeSort X) #) * the Arity of S) . o implies x is FinSequence of TS (DTConMSA X) )

set D = DTConMSA X;

set ar = the_arity_of o;

set cr = the carrier of S;

A1: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;

( 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 A2: dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

assume x in (((FreeSort X) #) * the Arity of S) . o ; :: thesis: x is FinSequence of TS (DTConMSA X)

then x in product ((FreeSort X) * (the_arity_of o)) by A1, Th1;

then consider f being Function such that

A3: x = f and

A4: dom f = dom ((FreeSort X) * (the_arity_of o)) and

A5: for y being object st y in dom ((FreeSort X) * (the_arity_of o)) holds

f . y in ((FreeSort X) * (the_arity_of o)) . y by CARD_3:def 5;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then reconsider f = f as FinSequence by A4, A2, FINSEQ_1:def 2;

rng f c= TS (DTConMSA X)

proof

then reconsider f = f as FinSequence of TS (DTConMSA X) by FINSEQ_1:def 4;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in TS (DTConMSA X) )

assume a in rng f ; :: thesis: a in TS (DTConMSA X)

then consider b being object such that

A6: b in dom f and

A7: f . b = a by FUNCT_1:def 3;

A8: a in ((FreeSort X) * (the_arity_of o)) . b by A4, A5, A6, A7;

reconsider b = b as Nat by A6;

((FreeSort X) * (the_arity_of o)) . b = (FreeSort X) . ((the_arity_of o) . b) by A4, A6, FUNCT_1:12

.= (FreeSort X) . ((the_arity_of o) /. b) by A4, A2, A6, PARTFUN1:def 6

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

.= { s where s is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . ((the_arity_of o) /. b) & s = root-tree [x,((the_arity_of o) /. b)] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = s . {} & the_result_sort_of o1 = (the_arity_of o) /. b ) ) } ;

then ex e being Element of TS (DTConMSA X) st

( a = e & ( ex x being set st

( x in X . ((the_arity_of o) /. b) & e = root-tree [x,((the_arity_of o) /. b)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = e . {} & the_result_sort_of o = (the_arity_of o) /. b ) ) ) by A8;

hence a in TS (DTConMSA X) ; :: thesis: verum

end;assume a in rng f ; :: thesis: a in TS (DTConMSA X)

then consider b being object such that

A6: b in dom f and

A7: f . b = a by FUNCT_1:def 3;

A8: a in ((FreeSort X) * (the_arity_of o)) . b by A4, A5, A6, A7;

reconsider b = b as Nat by A6;

((FreeSort X) * (the_arity_of o)) . b = (FreeSort X) . ((the_arity_of o) . b) by A4, A6, FUNCT_1:12

.= (FreeSort X) . ((the_arity_of o) /. b) by A4, A2, A6, PARTFUN1:def 6

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

.= { s where s is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . ((the_arity_of o) /. b) & s = root-tree [x,((the_arity_of o) /. b)] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = s . {} & the_result_sort_of o1 = (the_arity_of o) /. b ) ) } ;

then ex e being Element of TS (DTConMSA X) st

( a = e & ( ex x being set st

( x in X . ((the_arity_of o) /. b) & e = root-tree [x,((the_arity_of o) /. b)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = e . {} & the_result_sort_of o = (the_arity_of o) /. b ) ) ) by A8;

hence a in TS (DTConMSA X) ; :: thesis: verum

f = x by A3;

hence x is FinSequence of TS (DTConMSA X) ; :: thesis: verum