let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty 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 non-empty ManySortedSet of the carrier of S; :: thesis: 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)); :: thesis: 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; :: thesis: 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))); :: thesis: 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)); :: thesis: ( p = q implies R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q )
assume p = q ; :: thesis: 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; :: thesis: verum