let S be non void Signature; :: thesis: for X being non empty ManySortedSet of
for f being term-transformation of S,X
for s being SortSymbol of S
for p being FinSequence of the Sorts of (Free S,X) . s holds
( f * p is FinSequence of the Sorts of (Free S,X) . s & card (f * p) = len p )
let X be non empty ManySortedSet of ; :: thesis: for f being term-transformation of S,X
for s being SortSymbol of S
for p being FinSequence of the Sorts of (Free S,X) . s holds
( f * p is FinSequence of the Sorts of (Free S,X) . s & card (f * p) = len p )
set A = Free S,X;
let f be term-transformation of S,X; :: thesis: for s being SortSymbol of S
for p being FinSequence of the Sorts of (Free S,X) . s holds
( f * p is FinSequence of the Sorts of (Free S,X) . s & card (f * p) = len p )
let s be SortSymbol of S; :: thesis: for p being FinSequence of the Sorts of (Free S,X) . s holds
( f * p is FinSequence of the Sorts of (Free S,X) . s & card (f * p) = len p )
let p be FinSequence of the Sorts of (Free S,X) . s; :: thesis: ( f * p is FinSequence of the Sorts of (Free S,X) . s & card (f * p) = len p )
( Union the Sorts of (Free S,X) = {} or Union the Sorts of (Free S,X) <> {} ) ;
then Z1: ( dom the Sorts of (Free S,X) = the carrier of S & dom f = Union the Sorts of (Free S,X) ) by FUNCT_2:def 1, PARTFUN1:def 4;
the Sorts of (Free S,X) . s in rng the Sorts of (Free S,X) by Z1, FUNCT_1:def 5;
then the Sorts of (Free S,X) . s c= Union the Sorts of (Free S,X) by ZFMISC_1:92;
then rng p c= dom f by Z1, XBOOLE_1:1;
then Z7: dom (f * p) = dom p by RELAT_1:46;
dom p = Seg (len p) by FINSEQ_1:def 3;
then Z2: f * p is FinSequence by Z7, FINSEQ_1:def 2;
rng (f * p) c= the Sorts of (Free S,X) . s

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (f * p) or z in the Sorts of (Free S,X) . s )
assume z in rng (f * p) ; :: thesis: z in the Sorts of (Free S,X) . s
then consider i being set such that
V1: ( i in dom (f * p) & z = (f * p) . i ) by FUNCT_1:def 5;
p . i in rng p by Z7, V1, FUNCT_1:def 5;
then f . (p . i) in the Sorts of (Free S,X) . s by ThTr;
hence z in the Sorts of (Free S,X) . s by V1, FUNCT_1:22; :: thesis: verum

end;

hence f * p is FinSequence of the Sorts of (Free S,X) . s by Z2, FINSEQ_1:def 4; :: thesis: card (f * p) = len p
then reconsider q = f * p as FinSequence of the Sorts of (Free S,X) . s ;
thus card (f * p) = len q
.= len p by Z7, FINSEQ_3:31 ; :: thesis: verum