let R be ManySortedRelation of (Free (S,X)); :: thesis: ( R is V6() implies ( R is NF-var & R is invariant & R is stable ) )
assume A1: R is V6() ; :: 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 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; :: thesis: 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; :: thesis: verum