let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))
let X be non-empty ManySortedSet of S; :: thesis: for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X)); :: thesis: for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))
let g be ManySortedFunction of (Free (S,X)),(Free (S,X)); :: thesis: ( g is_homomorphism Free (S,X), Free (S,X) implies for s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s)) )
assume g is_homomorphism Free (S,X), Free (S,X) ; :: thesis: for s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))
then A1: g is Endomorphism of Free (S,X) by MSUALG_6:def 2;
let s be SortSymbol of S; :: thesis: for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))
let a be Element of (Free (S,X)),s; :: thesis: nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))
nf (a,(R . s)) is_a_normal_form_of a,R . s by REWRITE1:54;
then A2: R . s reduces a, nf (a,(R . s)) ;
defpred S₁[ set ] means nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . $1),(R . s));
A3: S₁[ nf (a,(R . s))] ;
A4: for b, c being set st [b,c] in R . s & S₁[c] holds
S₁[b]

proof

let b, c be set ; :: thesis: ( [b,c] in R . s & S₁[c] implies S₁[b] )
assume A5: [b,c] in R . s ; :: thesis: ( not S₁[c] or S₁[b] )
then reconsider x = b, y = c as Element of (Free (S,X)),s by ZFMISC_1:87;
A6: [((g . s) . x),((g . s) . y)] in R . s by A1, A5, MSUALG_6:def 9;
assume S₁[c] ; :: thesis: S₁[b]
hence S₁[b] by A6, REWRITE1:29, REWRITE1:55; :: thesis: verum

end;

S₁[a] from MSAFREE4:sch 6(A3, A2, A4);
hence nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s)) ; :: thesis: verum