let S be non void Signature; :: thesis: for X being non empty ManySortedSet of the carrier of S
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 the carrier of S; :: 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 )
A1: ( Union the Sorts of (Free (S,X)) = {} or Union the Sorts of (Free (S,X)) <> {} ) ;
A2: dom the Sorts of (Free (S,X)) = the carrier of S by PARTFUN1:def 2;
A3: dom f = Union the Sorts of (Free (S,X)) by A1, FUNCT_2:def 1;
the Sorts of (Free (S,X)) . s in rng the Sorts of (Free (S,X)) by A2, FUNCT_1:def 3;
then the Sorts of (Free (S,X)) . s c= Union the Sorts of (Free (S,X)) by ZFMISC_1:74;
then rng p c= dom f by A3;
then A4: dom (f * p) = dom p by RELAT_1:27;
dom p = Seg (len p) by FINSEQ_1:def 3;
then A5: f * p is FinSequence by A4, FINSEQ_1:def 2;
A6: rng (f * p) c= the Sorts of (Free (S,X)) . s
proof
let z be object ; :: 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 object such that
A7: i in dom (f * p) and
A8: z = (f * p) . i by FUNCT_1:def 3;
p . i in rng p by A4, A7, FUNCT_1:def 3;
then f . (p . i) in the Sorts of (Free (S,X)) . s by Th129;
hence z in the Sorts of (Free (S,X)) . s by A7, A8, FUNCT_1:12; :: thesis: verum
end;
hence f * p is FinSequence of the Sorts of (Free (S,X)) . s by A5, FINSEQ_1:def 4; :: thesis: card (f * p) = len p
reconsider q = f * p as FinSequence of the Sorts of (Free (S,X)) . s by A5, A6, FINSEQ_1:def 4;
thus card (f * p) = len q
.= len p by A4, FINSEQ_3:29 ; :: thesis: verum