let S be non void Signature; :: thesis: for X being non empty ManySortedSet of the carrier of S
for f being UnOp of (Union the Sorts of (Free (S,X))) holds
( f is term-transformation of S,X iff for s being SortSymbol of S
for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s )
let X be non empty ManySortedSet of the carrier of S; :: thesis: for f being UnOp of (Union the Sorts of (Free (S,X))) holds
( f is term-transformation of S,X iff for s being SortSymbol of S
for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s )
A1: dom the Sorts of (Free (S,X)) = the carrier of S by PARTFUN1:def 2;
let f be UnOp of (Union the Sorts of (Free (S,X))); :: thesis: ( f is term-transformation of S,X iff for s being SortSymbol of S
for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s )
A2: dom f = Union the Sorts of (Free (S,X)) by FUNCT_2:52;

hereby :: thesis: ( ( for s being SortSymbol of S
for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s ) implies f is term-transformation of S,X )

assume A3: f is term-transformation of S,X ; :: thesis: for s being SortSymbol of S
for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s
let s be SortSymbol of S; :: thesis: for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s
A4: f .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s by A3, Def56;
the Sorts of (Free (S,X)) . s in rng the Sorts of (Free (S,X)) by A1, FUNCT_1:def 3;
then A5: the Sorts of (Free (S,X)) . s c= Union the Sorts of (Free (S,X)) by ZFMISC_1:74;
let a be set ; :: thesis: ( a in the Sorts of (Free (S,X)) . s implies f . a in the Sorts of (Free (S,X)) . s )
assume a in the Sorts of (Free (S,X)) . s ; :: thesis: f . a in the Sorts of (Free (S,X)) . s
then f . a in f .: ( the Sorts of (Free (S,X)) . s) by A2, A5, FUNCT_1:def 6;
hence f . a in the Sorts of (Free (S,X)) . s by A4; :: thesis: verum

end;

assume A6: for s being SortSymbol of S
for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s ; :: thesis: f is term-transformation of S,X
let s be SortSymbol of S; :: according to ABCMIZ_1:def 56 :: thesis: f .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: ( the Sorts of (Free (S,X)) . s) or x in the Sorts of (Free (S,X)) . s )
assume x in f .: ( the Sorts of (Free (S,X)) . s) ; :: thesis: x in the Sorts of (Free (S,X)) . s
then ex a being object st
( a in dom f & a in the Sorts of (Free (S,X)) . s & x = f . a ) by FUNCT_1:def 6;
hence x in the Sorts of (Free (S,X)) . s by A6; :: thesis: verum