set A = NFAlgebra R;
A1:
the Sorts of (NFAlgebra R) = NForms R
by Def20;
thus
FreeGen X is ManySortedSubset of the Sorts of (NFAlgebra R)
MSAFREE4:def 7 ( NFAlgebra R is inheriting_operations & NFAlgebra R is free_in_itself )proof
let i be
object ;
PBOOLE:def 2,
PBOOLE:def 18 ( not i in the carrier of S or (FreeGen X) . i c= the Sorts of (NFAlgebra R) . i )
assume
i in the
carrier of
S
;
(FreeGen X) . i c= the Sorts of (NFAlgebra R) . i
then reconsider s =
i as
SortSymbol of
S ;
let x be
object ;
TARSKI:def 3 ( not x in (FreeGen X) . i or x in the Sorts of (NFAlgebra R) . i )
assume A2:
x in (FreeGen X) . i
;
x in the Sorts of (NFAlgebra R) . i
Free (
S,
X)
= FreeMSA X
by MSAFREE3:31;
then
(FreeGen X) . s c= the
Sorts of
(Free (S,X)) . s
by PBOOLE:def 2, PBOOLE:def 18;
then reconsider x =
x as
Element of
(Free (S,X)),
s by A2;
(
x is_a_normal_form_wrt R . s &
R . s reduces x,
x )
by A2, Def18, REWRITE1:12;
then
(
x is_a_normal_form_of x,
R . s &
nf (
x,
(R . s))
is_a_normal_form_of x,
R . s )
by REWRITE1:54;
then
(
x = nf (
x,
(R . s)) &
(NForms R) . s = { (nf (y,(R . s))) where y is Element of (Free (S,X)),s : verum } )
by Def19, REWRITE1:53;
hence
x in the
Sorts of
(NFAlgebra R) . i
by A1;
verum
end;
hereby MSAFREE4:def 8 NFAlgebra R is free_in_itself
let o be
OperSymbol of
S;
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of (NFAlgebra R) . (the_result_sort_of o) holds
( p in Args (o,(NFAlgebra R)) & (Den (o,(NFAlgebra R))) . p = (Den (o,(Free (S,X)))) . p )let p be
FinSequence;
( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of (NFAlgebra R) . (the_result_sort_of o) implies ( p in Args (o,(NFAlgebra R)) & (Den (o,(NFAlgebra R))) . p = (Den (o,(Free (S,X)))) . p ) )assume A3:
(
p in Args (
o,
(Free (S,X))) &
(Den (o,(Free (S,X)))) . p in the
Sorts of
(NFAlgebra R) . (the_result_sort_of o) )
;
( p in Args (o,(NFAlgebra R)) & (Den (o,(NFAlgebra R))) . p = (Den (o,(Free (S,X)))) . p )then A4:
(
dom p = dom (the_arity_of o) &
dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) )
by MSUALG_3:6, PRALG_2:3;
reconsider q =
p as
FinSequence ;
(Den (o,(Free (S,X)))) . p in { (nf (z,(R . (the_result_sort_of o)))) where z is Element of the Sorts of (Free (S,X)) . (the_result_sort_of o) : verum }
by A1, A3, Def19;
then consider z being
Element of the
Sorts of
(Free (S,X)) . (the_result_sort_of o) such that A5:
(Den (o,(Free (S,X)))) . p = nf (
z,
(R . (the_result_sort_of o)))
;
A6:
(Den (o,(Free (S,X)))) . p is_a_normal_form_of z,
R . (the_result_sort_of o)
by A5, REWRITE1:54;
A7:
now for i being object st i in dom p holds
not p . i nin ((NForms R) * (the_arity_of o)) . ilet i be
object ;
( i in dom p implies not p . i nin ((NForms R) * (the_arity_of o)) . i )assume A8:
i in dom p
;
not p . i nin ((NForms R) * (the_arity_of o)) . ithen A9:
the
Sorts of
(Free (S,X)) . ((the_arity_of o) . i) = ( the Sorts of (Free (S,X)) * (the_arity_of o)) . i
by A4, FUNCT_1:13;
reconsider j =
i as
Element of
NAT by A8;
reconsider ai =
(the_arity_of o) . i as
SortSymbol of
S by A4, A8, FUNCT_1:102;
A10:
ai = (the_arity_of o) /. j
by A8, A4, PARTFUN1:def 6;
Args (
o,
(Free (S,X)))
= product ( the Sorts of (Free (S,X)) * (the_arity_of o))
by PRALG_2:3;
then reconsider pj =
p . i as
Element of the
Sorts of
(Free (S,X)) . ((the_arity_of o) . i) by A3, A9, A8, A4, CARD_3:9;
assume
p . i nin ((NForms R) * (the_arity_of o)) . i
;
contradictionthen
p . i nin (NForms R) . ((the_arity_of o) . i)
by A4, A8, FUNCT_1:13;
then
pj nin { (nf (b,(R . ((the_arity_of o) /. i)))) where b is Element of the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) : verum }
by A10, Def19;
then
(
nf (
pj,
(R . ((the_arity_of o) . i)))
is_a_normal_form_of pj,
R . ((the_arity_of o) . i) & ( for
a being
Element of the
Sorts of
(Free (S,X)) . ((the_arity_of o) . i) holds
pj <> nf (
a,
(R . ((the_arity_of o) . i))) ) )
by A10, REWRITE1:54;
then
(
R . ((the_arity_of o) . i) reduces pj,
nf (
pj,
(R . ((the_arity_of o) . i))) &
nf (
pj,
(R . ((the_arity_of o) . i)))
<> pj )
;
then consider x being
object such that A11:
[pj,x] in R . ((the_arity_of o) . i)
by REWRITE1:33, REWRITE1:def 5;
reconsider x =
x as
Element of the
Sorts of
(Free (S,X)) . ((the_arity_of o) . i) by A11, ZFMISC_1:87;
set f =
transl (
o,
j,
q,
(Free (S,X)));
A12:
(transl (o,j,q,(Free (S,X)))) . pj =
(Den (o,(Free (S,X)))) . (q +* (j,pj))
by A10, MSUALG_6:def 4
.=
(Den (o,(Free (S,X)))) . p
by FUNCT_7:35
;
[((transl (o,j,q,(Free (S,X)))) . pj),((transl (o,j,q,(Free (S,X)))) . x)] in R . (the_result_sort_of o)
by A11, A3, A8, A4, A10, MSUALG_6:def 5, MSUALG_6:def 8;
hence
contradiction
by A6, A12, REWRITE1:def 5;
verum end;
dom ((NForms R) * (the_arity_of o)) = dom (the_arity_of o)
by A1, PRALG_2:3;
then
p in product ((NForms R) * (the_arity_of o))
by A4, A7, CARD_3:9;
hence
p in Args (
o,
(NFAlgebra R))
by A1, PRALG_2:3;
(Den (o,(NFAlgebra R))) . p = (Den (o,(Free (S,X)))) . phence (Den (o,(NFAlgebra R))) . p =
nf (
((Den (o,(Free (S,X)))) . p),
(R . (the_result_sort_of o)))
by Def20
.=
(Den (o,(Free (S,X)))) . p
by A6, Th17
;
verum
end;
let f be ManySortedFunction of FreeGen X, the Sorts of (NFAlgebra R); MSAFREE4:def 9 for G being ManySortedSubset of the Sorts of (NFAlgebra R) st G = FreeGen X holds
ex h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st
( h is_homomorphism NFAlgebra R, NFAlgebra R & f = h || G )
let G be ManySortedSubset of the Sorts of (NFAlgebra R); ( G = FreeGen X implies ex h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st
( h is_homomorphism NFAlgebra R, NFAlgebra R & f = h || G ) )
assume A13:
G = FreeGen X
; ex h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st
( h is_homomorphism NFAlgebra R, NFAlgebra R & f = h || G )
reconsider H = FreeGen X as GeneratorSet of Free (S,X) by MSAFREE3:31;
( the Sorts of (NFAlgebra R) = NForms R & H is_transformable_to NForms R & H is_transformable_to the Sorts of (Free (S,X)) )
by Def20, Th21;
then A14:
( the Sorts of (NFAlgebra R) c= the Sorts of (Free (S,X)) & rngs f c= the Sorts of (NFAlgebra R) & doms f = H )
by MSSUBFAM:17, PBOOLE:def 18;
then
( rngs f c= the Sorts of (Free (S,X)) & FreeMSA X = Free (S,X) )
by PBOOLE:13, MSAFREE3:31;
then
( f is ManySortedFunction of H, the Sorts of (Free (S,X)) & H is free )
by A14, Th21, EQUATION:4;
then consider g being ManySortedFunction of (Free (S,X)),(Free (S,X)) such that
A15:
( g is_homomorphism Free (S,X), Free (S,X) & g || H = f )
;
deffunc H2( SortSymbol of S, Element of (NFAlgebra R),S) -> set = nf (((g . S) . X),(R . S));
defpred S1[ object , object , object ] means R = nf (((g . S) . X),(R . S));
A16:
for s, x being object st s in the carrier of S & x in the Sorts of (NFAlgebra R) . s holds
ex y being object st
( y in the Sorts of (NFAlgebra R) . s & S1[s,x,y] )
proof
let s,
x be
object ;
( s in the carrier of S & x in the Sorts of (NFAlgebra R) . s implies ex y being object st
( y in the Sorts of (NFAlgebra R) . s & S1[s,x,y] ) )
assume A17:
s in the
carrier of
S
;
( not x in the Sorts of (NFAlgebra R) . s or ex y being object st
( y in the Sorts of (NFAlgebra R) . s & S1[s,x,y] ) )
assume A18:
x in the
Sorts of
(NFAlgebra R) . s
;
ex y being object st
( y in the Sorts of (NFAlgebra R) . s & S1[s,x,y] )
reconsider t =
s as
SortSymbol of
S by A17;
reconsider z =
x as
Element of
(NFAlgebra R),
t by A18;
take y =
H2(
t,
z);
( y in the Sorts of (NFAlgebra R) . s & S1[s,x,y] )
(NForms R) . t c= the
Sorts of
(Free (S,X)) . t
by PBOOLE:def 2, PBOOLE:def 18;
then reconsider a =
(g . t) . z as
Element of
(Free (S,X)),
t by A1, FUNCT_2:5;
y = nf (
a,
(R . t))
;
then
y in { (nf (u,(R . t))) where u is Element of (Free (S,X)),t : verum }
;
hence
y in the
Sorts of
(NFAlgebra R) . s
by A1, Def19;
S1[s,x,y]
thus
S1[
s,
x,
y]
;
verum
end;
consider h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) such that
A19:
for s, x being object st s in the carrier of S & x in the Sorts of (NFAlgebra R) . s holds
( (h . s) . x in the Sorts of (NFAlgebra R) . s & S1[s,x,(h . s) . x] )
from YELLOW18:sch 23(A16);
take
h
; ( h is_homomorphism NFAlgebra R, NFAlgebra R & f = h || G )
thus
h is_homomorphism NFAlgebra R, NFAlgebra R
f = h || Gproof
let o be
OperSymbol of
S;
MSUALG_3:def 7 ( Args (o,(NFAlgebra R)) = {} or for b1 being Element of Args (o,(NFAlgebra R)) holds (h . (the_result_sort_of o)) . ((Den (o,(NFAlgebra R))) . b1) = (Den (o,(NFAlgebra R))) . (h # b1) )
assume
Args (
o,
(NFAlgebra R))
<> {}
;
for b1 being Element of Args (o,(NFAlgebra R)) holds (h . (the_result_sort_of o)) . ((Den (o,(NFAlgebra R))) . b1) = (Den (o,(NFAlgebra R))) . (h # b1)
let x be
Element of
Args (
o,
(NFAlgebra R));
(h . (the_result_sort_of o)) . ((Den (o,(NFAlgebra R))) . x) = (Den (o,(NFAlgebra R))) . (h # x)
(NForms R) * (the_arity_of o) c= the
Sorts of
(Free (S,X)) * (the_arity_of o)
by Th15, PBOOLE:def 18;
then
product ((NForms R) * (the_arity_of o)) c= product ( the Sorts of (Free (S,X)) * (the_arity_of o))
by Th16;
then
product ((NForms R) * (the_arity_of o)) c= Args (
o,
(Free (S,X)))
by PRALG_2:3;
then
(
Args (
o,
(NFAlgebra R))
c= Args (
o,
(Free (S,X))) &
x in Args (
o,
(NFAlgebra R)) )
by A1, PRALG_2:3;
then reconsider y =
x as
Element of
Args (
o,
(Free (S,X))) ;
A20:
for
s being
SortSymbol of
S for
x being
Element of
(NFAlgebra R),
s holds
(h . s) . x = nf (
((g . s) . x),
(R . s))
by A19;
reconsider Dy =
(Den (o,(Free (S,X)))) . y as
Element of
(Free (S,X)),
(the_result_sort_of o) by FUNCT_2:15;
(Den (o,(NFAlgebra R))) . x in Result (
o,
(NFAlgebra R))
;
then
(Den (o,(NFAlgebra R))) . x in the
Sorts of
(NFAlgebra R) . (the_result_sort_of o)
by FUNCT_2:15;
hence (h . (the_result_sort_of o)) . ((Den (o,(NFAlgebra R))) . x) =
nf (
((g . (the_result_sort_of o)) . ((Den (o,(NFAlgebra R))) . x)),
(R . (the_result_sort_of o)))
by A19
.=
nf (
((g . (the_result_sort_of o)) . (nf (((Den (o,(Free (S,X)))) . x),(R . (the_result_sort_of o))))),
(R . (the_result_sort_of o)))
by Def20
.=
nf (
((g . (the_result_sort_of o)) . Dy),
(R . (the_result_sort_of o)))
by A15, Th80
.=
nf (
((Den (o,(Free (S,X)))) . (g # y)),
(R . (the_result_sort_of o)))
by A15
.=
nf (
((Den (o,(NFAlgebra R))) . (h # x)),
(R . (the_result_sort_of o)))
by A15, A20, Th85
.=
nf (
(nf (((Den (o,(Free (S,X)))) . (h # x)),(R . (the_result_sort_of o)))),
(R . (the_result_sort_of o)))
by Def20
.=
nf (
((Den (o,(Free (S,X)))) . (h # x)),
(R . (the_result_sort_of o)))
by Th18
.=
(Den (o,(NFAlgebra R))) . (h # x)
by Def20
;
verum
end;
let a be Element of S; PBOOLE:def 21 f . a = (h || G) . a
A21:
( dom (f . a) = H . a & dom ((h || G) . a) = G . a )
by FUNCT_2:def 1;
hence
dom (f . a) = dom ((h || G) . a)
by A13; FUNCT_1:def 11 for b1 being object holds
( not b1 in proj1 (f . a) or (f . a) . b1 = ((h || G) . a) . b1 )
let x be object ; ( not x in proj1 (f . a) or (f . a) . x = ((h || G) . a) . x )
assume A22:
x in dom (f . a)
; (f . a) . x = ((h || G) . a) . x
A23:
G . a c= the Sorts of (NFAlgebra R) . a
by PBOOLE:def 2, PBOOLE:def 18;
reconsider fax = (f . a) . x as Element of (NFAlgebra R),a by A22, FUNCT_2:5;
the Sorts of (NFAlgebra R) = NForms R
by Def20;
hence (f . a) . x =
nf (fax,(R . a))
by Th79
.=
nf ((((g . a) | (H . a)) . x),(R . a))
by A15, MSAFREE:def 1
.=
nf (((g . a) . x),(R . a))
by A22, FUNCT_1:49
.=
(h . a) . x
by A23, A13, A21, A22, A19
.=
((h . a) | (G . a)) . x
by A13, A22, FUNCT_1:49
.=
((h || G) . a) . x
by MSAFREE:def 1
;
verum