let R be ManySortedRelation of (Free (S,X)); ( R is V6() implies ( R is NF-var & R is invariant & R is stable ) )
assume A1:
R is V6()
; ( R is NF-var & R is invariant & R is stable )
thus
R is NF-var
( R is invariant & R is stable )
thus
R is invariant
by A1; R is stable
let h be Endomorphism of Free (S,X); MSUALG_6:def 9 for b1 being Element of the carrier of S
for b2, b3 being set holds
( not [b2,b3] in R . b1 or [((h . b1) . b2),((h . b1) . b3)] in R . b1 )
let s be SortSymbol of S; for b1, b2 being set holds
( not [b1,b2] in R . s or [((h . s) . b1),((h . s) . b2)] in R . s )
thus
for b1, b2 being set holds
( not [b1,b2] in R . s or [((h . s) . b1),((h . s) . b2)] in R . s )
by A1; verum