let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for x being set
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for a being SortSymbol of S st x in (NForms R) . a holds
nf (x,(R . a)) = x
let X be non-empty ManySortedSet of S; :: thesis: for x being set
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for a being SortSymbol of S st x in (NForms R) . a holds
nf (x,(R . a)) = x
let x be set ; :: thesis: for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for a being SortSymbol of S st x in (NForms R) . a holds
nf (x,(R . a)) = x
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X)); :: thesis: for a being SortSymbol of S st x in (NForms R) . a holds
nf (x,(R . a)) = x
let a be SortSymbol of S; :: thesis: ( x in (NForms R) . a implies nf (x,(R . a)) = x )
assume x in (NForms R) . a ; :: thesis: nf (x,(R . a)) = x
then x in { (nf (z,(R . a))) where z is Element of (Free (S,X)),a : verum } by Def19;
then ex z being Element of (Free (S,X)),a st x = nf (z,(R . a)) ;
hence nf (x,(R . a)) = x by Th18; :: thesis: verum