let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X)))
for q being Element of Args (o,(NFAlgebra R)) st p = q holds
R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q
let X be V5() ManySortedSet of the carrier of S; for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X)))
for q being Element of Args (o,(NFAlgebra R)) st p = q holds
R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q
let R be invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)); for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X)))
for q being Element of Args (o,(NFAlgebra R)) st p = q holds
R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q
let o be OperSymbol of S; for p being Element of Args (o,(Free (S,X)))
for q being Element of Args (o,(NFAlgebra R)) st p = q holds
R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q
let p be Element of Args (o,(Free (S,X))); for q being Element of Args (o,(NFAlgebra R)) st p = q holds
R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q
let q be Element of Args (o,(NFAlgebra R)); ( p = q implies R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q )
assume
p = q
; R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q
then
(canonical_homomorphism (NFAlgebra R)) # p = q
by MSAFREE4:66;
hence
R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q
by Th98; verum