set T = NFAlgebra R;
let o be OperSymbol of S; :: according to MSAFREE5:def 32 :: thesis: for p being Element of Args (o,(NFAlgebra R)) st (Den (o,(NFAlgebra R))) . p = (Den (o,(Free (S,X)))) . p holds
for s being SortSymbol of S
for x1, x2 being Element of X . s holds (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # p)
let p be Element of Args (o,(NFAlgebra R)); :: thesis: ( (Den (o,(NFAlgebra R))) . p = (Den (o,(Free (S,X)))) . p implies for s being SortSymbol of S
for x1, x2 being Element of X . s holds (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # p) )
Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) by MSAFREE4:41;
then reconsider q = p as Element of Args (o,(Free (S,X))) ;
assume A1: (Den (o,(NFAlgebra R))) . p = (Den (o,(Free (S,X)))) . p ; :: thesis: for s being SortSymbol of S
for x1, x2 being Element of X . s holds (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # p)
let s be SortSymbol of S; :: thesis: for x1, x2 being Element of X . s holds (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # p)
let x1, x2 be Element of X . s; :: thesis: (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # p)
set h = Hom ((NFAlgebra R),x1,x2);
set H = Hom ((Free (S,X)),x1,x2);
AA: (Hom ((NFAlgebra R),x1,x2)) # p = (Hom ((Free (S,X)),x1,x2)) # q

proof

B1: ( dom ((Hom ((NFAlgebra R),x1,x2)) # p) = dom (the_arity_of o) & dom (the_arity_of o) = dom ((Hom ((Free (S,X)),x1,x2)) # q) & dom p = dom (the_arity_of o) & dom (the_arity_of o) = dom q ) by MSUALG_3:6;
hence len ((Hom ((NFAlgebra R),x1,x2)) # p) = len ((Hom ((Free (S,X)),x1,x2)) # q) by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((Hom ((NFAlgebra R),x1,x2)) # p) or ((Hom ((NFAlgebra R),x1,x2)) # p) . b₁ = ((Hom ((Free (S,X)),x1,x2)) # q) . b₁ )
let i be Nat; :: thesis: ( not 1 <= i or not i <= len ((Hom ((NFAlgebra R),x1,x2)) # p) or ((Hom ((NFAlgebra R),x1,x2)) # p) . i = ((Hom ((Free (S,X)),x1,x2)) # q) . i )
assume B0: ( 1 <= i & i <= len ((Hom ((NFAlgebra R),x1,x2)) # p) ) ; :: thesis: ((Hom ((NFAlgebra R),x1,x2)) # p) . i = ((Hom ((Free (S,X)),x1,x2)) # q) . i
B3: ( ((Hom ((NFAlgebra R),x1,x2)) # p) . i = ((Hom ((NFAlgebra R),x1,x2)) . ((the_arity_of o) /. i)) . (p . i) & ((Hom ((Free (S,X)),x1,x2)) # q) . i = ((Hom ((Free (S,X)),x1,x2)) . ((the_arity_of o) /. i)) . (q . i) ) by B1, B0, FINSEQ_3:25, MSUALG_3:def 6;
A8: ( p . i = p /. i & q . i = q /. i ) by B1, B0, FINSEQ_3:25, PARTFUN1:def 6;
then ( q /. i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) & p /. i in the Sorts of (NFAlgebra R) . ((the_arity_of o) /. i) ) by B1, B0, FINSEQ_3:25, MSUALG_6:2;
then A7: ( the_sort_of (p /. i) = (the_arity_of o) /. i & (the_arity_of o) /. i = the_sort_of (q /. i) ) by SORT;
then ((Hom ((Free (S,X)),x1,x2)) . ((the_arity_of o) /. i)) . (p /. i) = (Hom ((NFAlgebra R),x1,x2)) . (p /. i) by Th112;
hence ((Hom ((NFAlgebra R),x1,x2)) # p) . i = ((Hom ((Free (S,X)),x1,x2)) # q) . i by A7, A8, B3, ABBR; :: thesis: verum

end;

assume A2: (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) <> (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # p) ; :: thesis: contradiction
Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) by MSAFREE4:41;
then reconsider hp = (Hom ((NFAlgebra R),x1,x2)) # p as Element of Args (o,(Free (S,X))) ;
A4: ( R . (the_result_sort_of o) reduces o -term hp,(Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) & o -term hp = (Den (o,(Free (S,X)))) . hp ) by Th69, MSAFREE4:13;
then consider rs being RedSequence of R . (the_result_sort_of o) such that
A3: ( rs . 1 = (Den (o,(Free (S,X)))) . hp & rs . (len rs) = (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # p) ) ;
A7: ( len rs <> 1 & 0 + 1 <= len rs ) by A2, A3, NAT_1:13;
then 1 < len rs by XXREAL_0:1;
then 1 + 1 <= len rs by NAT_1:13;
then ( 1 + 1 in dom rs & 1 in dom rs ) by A7, FINSEQ_3:25;
then A2: [((Den (o,(Free (S,X)))) . hp),(rs . 2)] in R . (the_result_sort_of o) by A3, REWRITE1:def 2;
then reconsider rsi = rs . 2 as Element of (Free (S,X)),(the_result_sort_of o) by ZFMISC_1:87;
B2: [(((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . (o -term hp)),(((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . rsi)] in R . (the_result_sort_of o) by A2, A4, MSUALG_6:def 9;
A8: ( (Den (o,(Free (S,X)))) . hp = ((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . q) & (Den (o,(Free (S,X)))) . q in Result (o,(Free (S,X))) & Result (o,(Free (S,X))) = the Sorts of (Free (S,X)) . (the_result_sort_of o) ) by AA, FUNCT_2:5, FUNCT_2:15, MSUALG_3:def 7, MSUALG_6:def 2;
then A9: ((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . hp) = (((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) * ((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o))) . ((Den (o,(Free (S,X)))) . q) by FUNCT_2:15
.= (((Hom ((Free (S,X)),x1,x2)) ** (Hom ((Free (S,X)),x1,x2))) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . q) by MSUALG_3:2
.= ((id the Sorts of (Free (S,X))) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . q) by Th157
.= (id ( the Sorts of (Free (S,X)) . (the_result_sort_of o))) . ((Den (o,(Free (S,X)))) . q) by MSUALG_3:def 1
.= (Den (o,(Free (S,X)))) . q by A8, FUNCT_1:18 ;
set T = NFAlgebra R;
set g = canonical_homomorphism (NFAlgebra R);
(Den (o,(NFAlgebra R))) . p in Result (o,(NFAlgebra R)) by FUNCT_2:5;
then (Den (o,(NFAlgebra R))) . p is Element of (NFAlgebra R),(the_result_sort_of o) by FUNCT_2:15;
then reconsider op = (Den (o,(NFAlgebra R))) . p as Element of (NFAlgebra R) ;
(Den (o,(NFAlgebra R))) . p = nf (((Den (o,(Free (S,X)))) . p),(R . (the_result_sort_of o))) by MSAFREE4:def 20;
then (Den (o,(NFAlgebra R))) . p is_a_normal_form_of (Den (o,(Free (S,X)))) . p,R . (the_result_sort_of o) by REWRITE1:54;
then (Den (o,(NFAlgebra R))) . p is_a_normal_form_wrt R . (the_result_sort_of o) ;
hence contradiction by A1, B2, A4, A9; :: thesis: verum