let S be non void Signature; 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; 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))); ( 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 ( ( 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
;
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)) . slet s be
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)) . sA4:
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 ;
( 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
;
f . a in the Sorts of (Free (S,X)) . sthen
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;
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
; f is term-transformation of S,X
let s be SortSymbol of S; ABCMIZ_1:def 56 f .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s
let x be object ; TARSKI:def 3 ( 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)
; 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; verum