let R be ManySortedRelation of (Free (S,X)); :: thesis: ( R is empty-yielding implies ( R is NF-var & R is invariant & R is stable ) )
assume A1: R is empty-yielding ; :: thesis: ( R is NF-var & R is invariant & R is stable )
thus R is NF-var :: thesis: ( R is invariant & R is stable )

proof

let s be SortSymbol of S; :: according to MSAFREE4:def 18 :: thesis: for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s
R . s is empty by A1;
hence for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s ; :: thesis: verum

end;

thus R is invariant by A1; :: thesis: R is stable
let h be Endomorphism of Free (S,X); :: according to MSUALG_6:def 9 :: thesis: for b₁ being Element of the carrier of S
for b₂, b₃ being set holds
( not [b₂,b₃] in R . b₁ or [((h . b₁) . b₂),((h . b₁) . b₃)] in R . b₁ )
let s be SortSymbol of S; :: thesis: for b₁, b₂ being set holds
( not [b₁,b₂] in R . s or [((h . s) . b₁),((h . s) . b₂)] in R . s )
thus for b₁, b₂ being set holds
( not [b₁,b₂] in R . s or [((h . s) . b₁),((h . s) . b₂)] in R . s ) by A1; :: thesis: verum