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 ((() #) * the Arity of S) . o holds
x is FinSequence of TS ()

let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for x being set st x in ((() #) * the Arity of S) . o holds
x is FinSequence of TS ()

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

let x be set ; :: thesis: ( x in ((() #) * the Arity of S) . o implies x is FinSequence of TS () )
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 () c= the carrier of S & dom () = the carrier of S ) by ;
then A2: dom (() * ()) = dom () by RELAT_1:27;
assume x in ((() #) * the Arity of S) . o ; :: thesis: x is FinSequence of TS ()
then x in product (() * ()) by ;
then consider f being Function such that
A3: x = f and
A4: dom f = dom (() * ()) and
A5: for y being object st y in dom (() * ()) holds
f . y in (() * ()) . y by CARD_3:def 5;
dom () = Seg (len ()) by FINSEQ_1:def 3;
then reconsider f = f as FinSequence by ;
rng f c= TS ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in TS () )
assume a in rng f ; :: thesis: a in TS ()
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 (() * ()) . b by A4, A5, A6, A7;
reconsider b = b as Nat by A6;
(() * ()) . b = () . (() . b) by
.= () . (() /. b) by
.= FreeSort (X,(() /. b)) by Def11
.= { s where s is Element of TS () : ( ex x being set st
( x in X . (() /. b) & s = root-tree [x,(() /. b)] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = s . {} & the_result_sort_of o1 = () /. b ) )
}
;
then ex e being Element of TS () st
( a = e & ( ex x being set st
( x in X . (() /. b) & e = root-tree [x,(() /. b)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = e . {} & the_result_sort_of o = () /. b ) ) ) by A8;
hence a in TS () ; :: thesis: verum
end;
then reconsider f = f as FinSequence of TS () by FINSEQ_1:def 4;
f = x by A3;
hence x is FinSequence of TS () ; :: thesis: verum