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))) holds R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)
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))) holds R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)
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))) holds R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)
let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) holds R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)
let p be Element of Args (o,(Free (S,X))); :: thesis: R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)
set T = NFAlgebra R;
set h = canonical_homomorphism (NFAlgebra R);
A1: o -term p = (Den (o,(Free (S,X)))) . p by MSAFREE4:13;
A2: the_sort_of (o -term p) = the_result_sort_of o by Th8;
((canonical_homomorphism (NFAlgebra R)) . (the_result_sort_of o)) . (o -term p) = (Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p) by A1, MSUALG_3:def 7, MSAFREE4:def 10;
then (Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p) = (canonical_homomorphism (NFAlgebra R)) . (o -term p) by A2, ABBR;
hence R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p) by A2, Th90; :: thesis: verum