let S be non void Signature; :: thesis: for X being non empty ManySortedSet of
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 ; :: 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 )
A0:
dom the Sorts of (Free S,X) = the carrier of S
by PARTFUN1:def 4;
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 )
A1:
dom f = Union the Sorts of (Free S,X)
by FUNCT_2:67;
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 Z0:
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) . slet 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) . sZ1:
f .: (the Sorts of (Free S,X) . s) c= the
Sorts of
(Free S,X) . s
by TT, Z0;
the
Sorts of
(Free S,X) . s in rng the
Sorts of
(Free S,X)
by A0, FUNCT_1:def 5;
then Z2:
the
Sorts of
(Free S,X) . s c= Union the
Sorts of
(Free S,X)
by ZFMISC_1:92;
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) . sthen
f . a in f .: (the Sorts of (Free S,X) . s)
by A1, Z2, FUNCT_1:def 12;
hence
f . a in the
Sorts of
(Free S,X) . s
by Z1;
:: thesis: verum
end;
assume A2:
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 set ; :: 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 set st
( a in dom f & a in the Sorts of (Free S,X) . s & x = f . a )
by FUNCT_1:def 12;
hence
x in the Sorts of (Free S,X) . s
by A2; :: thesis: verum