let S be OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for x being set st x in (((ParsedTerms X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)
let X be non-empty ManySortedSet of S; :: thesis: for o being OperSymbol of S
for x being set st x in (((ParsedTerms X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)
let o be OperSymbol of S; :: thesis: for x being set st x in (((ParsedTerms X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)
let x be set ; :: thesis: ( x in (((ParsedTerms X) #) * the Arity of S) . o implies x is FinSequence of TS (DTConOSA X) )
set D = DTConOSA X;
set ar = the_arity_of o;
A1: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
assume x in (((ParsedTerms X) #) * the Arity of S) . o ; :: thesis: x is FinSequence of TS (DTConOSA X)
then x in product ((ParsedTerms X) * (the_arity_of o)) by A1, MSAFREE:1;
then consider f being Function such that
A2: x = f and
A3: dom f = dom ((ParsedTerms X) * (the_arity_of o)) and
A4: for y being object st y in dom ((ParsedTerms X) * (the_arity_of o)) holds
f . y in ((ParsedTerms X) * (the_arity_of o)) . y by CARD_3:def 5;
A5: dom ((ParsedTerms X) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then reconsider f = f as FinSequence by A3, A5, FINSEQ_1:def 2;
rng f c= TS (DTConOSA X)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in TS (DTConOSA X) )
assume a in rng f ; :: thesis: a in TS (DTConOSA 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 ((ParsedTerms X) * (the_arity_of o)) . b by A3, A4, A6, A7;
reconsider b = b as Nat by A6;
((ParsedTerms X) * (the_arity_of o)) . b = (ParsedTerms X) . ((the_arity_of o) . b) by A3, A6, FUNCT_1:12
.= (ParsedTerms X) . ((the_arity_of o) /. b) by A3, A5, A6, PARTFUN1:def 6
.= ParsedTerms (X,((the_arity_of o) /. b)) by Def8
.= { s where s is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= (the_arity_of o) /. b & x in X . s1 & s = root-tree [x,s1] ) 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 (DTConOSA X) st
( a = e & ( ex s1 being Element of S ex x being object st
( s1 <= (the_arity_of o) /. b & x in X . s1 & e = root-tree [x,s1] ) 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 (DTConOSA X) ; :: thesis: verum

end;

then reconsider f = f as FinSequence of TS (DTConOSA X) by FINSEQ_1:def 4;
f = x by A2;
hence x is FinSequence of TS (DTConOSA X) ; :: thesis: verum