set T = NFAlgebra R;
let o be OperSymbol of S; MSAFREE5:def 32 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)); ( (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
; 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; 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; (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;
FINSEQ_1:def 17 for b1 being set holds
( not 1 <= b1 or not b1 <= len ((Hom ((NFAlgebra R),x1,x2)) # p) or ((Hom ((NFAlgebra R),x1,x2)) # p) . b1 = ((Hom ((Free (S,X)),x1,x2)) # q) . b1 )
let i be
Nat;
( 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) )
;
((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;
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)
; 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; verum