let S be non empty non void ManySortedSign ; for X0 being V5() countable ManySortedSet of S
for A0 being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free
let X0 be V5() countable ManySortedSet of S; for A0 being X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free
let A0 be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free
set A = A0;
A1:
FreeMSA X0 = Free (S,X0)
by MSAFREE3:31;
let G be GeneratorSet of A0; ( G = FreeGen X0 implies G is Equations (S,A0) -free )
assume A2:
G = FreeGen X0
; G is Equations (S,A0) -free
set T = Equations (S,A0);
let B be non-empty Equations (S,A0) -satisfying MSAlgebra over S; MSAFREE4:def 12 for f being ManySortedFunction of G, the Sorts of B ex h being ManySortedFunction of A0,B st
( h is_homomorphism A0,B & h || G = f )
let f be ManySortedFunction of G, the Sorts of B; ex h being ManySortedFunction of A0,B st
( h is_homomorphism A0,B & h || G = f )
reconsider f0 = f as ManySortedFunction of FreeGen X0, the Sorts of B by A2;
reconsider H = FreeGen X0 as free GeneratorSet of Free (S,X0) by A1;
consider g being ManySortedFunction of (Free (S,X0)),B such that
A3:
( g is_homomorphism Free (S,X0),B & g || H = f0 )
by MSAFREE:def 5;
the Sorts of A0 is MSSubset of (Free (S,X0))
by Def6;
then reconsider i = id the Sorts of A0 as ManySortedFunction of A0,(Free (S,X0)) by Th22;
take h = g ** i; ( h is_homomorphism A0,B & h || G = f )
thus
h is_homomorphism A0,B
h || G = fproof
let o be
OperSymbol of
S;
MSUALG_3:def 7 ( Args (o,A0) = {} or for b1 being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . b1) = (Den (o,B)) . (h # b1) )
assume
Args (
o,
A0)
<> {}
;
for b1 being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . b1) = (Den (o,B)) . (h # b1)
let x be
Element of
Args (
o,
A0);
(h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (Den (o,B)) . (h # x)
set s =
the_result_sort_of o;
(Den (o,A0)) . x in Result (
o,
A0)
;
then A4:
(Den (o,A0)) . x in the
Sorts of
A0 . (the_result_sort_of o)
by FUNCT_2:15;
A5:
i . (the_result_sort_of o) = id ( the Sorts of A0 . (the_result_sort_of o))
by MSUALG_3:def 1;
(
x in Args (
o,
A0) &
Args (
o,
A0)
c= Args (
o,
(Free (S,X0))) )
by Th41;
then reconsider x0 =
x as
Element of
Args (
o,
(Free (S,X0))) ;
set w = the
"1-1" ManySortedFunction of
X0, the
carrier of
S --> NAT;
(
(Den (o,A0)) . x is
Element of
Result (
o,
A0) &
(Den (o,(Free (S,X0)))) . x0 is
Element of
Result (
o,
(Free (S,X0))) )
;
then reconsider f1 =
(Den (o,A0)) . x,
f2 =
(Den (o,(Free (S,X0)))) . x0 as
Term of
S,
X0 by Th42;
reconsider f =
(Den (o,(Free (S,X0)))) . x0 as
Element of
(Free (S,X0)),
(the_result_sort_of o) by MSUALG_9:18;
reconsider fa =
((canonical_homomorphism A0) . (the_result_sort_of o)) . f as
Element of
(Free (S,X0)),
(the_result_sort_of o) by Th39;
f1 in the
Sorts of
A0 . (the_result_sort_of o)
by MSUALG_9:18;
then
f1 is
Element of
(Free (S,X0)),
(the_result_sort_of o)
by Th39;
then
(
f1 in the
Sorts of
(Free (S,X0)) . (the_result_sort_of o) &
f2 in the
Sorts of
(Free (S,X0)) . (the_result_sort_of o) )
by MSUALG_9:18;
then
(
f1 in FreeSort (
X0,
(the_result_sort_of o)) &
f2 in FreeSort (
X0,
(the_result_sort_of o)) )
by A1, MSAFREE:def 11;
then
(
the_sort_of f1 = the_result_sort_of o &
the_sort_of f2 = the_result_sort_of o )
by MSATERM:def 5;
then reconsider t2 =
# (
f1, the
"1-1" ManySortedFunction of
X0, the
carrier of
S --> NAT),
t1 =
# (
f2, the
"1-1" ManySortedFunction of
X0, the
carrier of
S --> NAT) as
Element of
(TermAlg S),
(the_result_sort_of o) by Th60;
A6:
f1 = ((canonical_homomorphism A0) . (the_result_sort_of o)) . f
by Th67;
A0 |= t1 '=' t2
by A6, Th71;
then
t1 '=' t2 in { e where e is Element of (Equations S) . (the_result_sort_of o) : A0 |= e }
;
then
(
t1 '=' t2 in (Equations (S,A0)) . (the_result_sort_of o) &
B |= Equations (
S,
A0) )
by Def14, Def11;
then A7:
(g . (the_result_sort_of o)) . f = (g . (the_result_sort_of o)) . fa
by A6, A3, Th74;
thus (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) =
((g . (the_result_sort_of o)) * (i . (the_result_sort_of o))) . ((Den (o,A0)) . x)
by MSUALG_3:2
.=
(g . (the_result_sort_of o)) . ((i . (the_result_sort_of o)) . ((Den (o,A0)) . x))
by A4, FUNCT_2:15
.=
(g . (the_result_sort_of o)) . ((Den (o,A0)) . x)
by A5, A4, FUNCT_1:18
.=
(g . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x0)
by A7, Th67
.=
(Den (o,B)) . (g # x0)
by A3
.=
(Den (o,B)) . (h # x)
by A8, MSUALG_3:def 6
;
verum
end;
now for x being object st x in the carrier of S holds
(h || G) . x = f . xlet x be
object ;
( x in the carrier of S implies (h || G) . x = f . x )assume
x in the
carrier of
S
;
(h || G) . x = f . xthen reconsider s =
x as
SortSymbol of
S ;
A12:
G . s c= the
Sorts of
A0 . s
by PBOOLE:def 2, PBOOLE:def 18;
(
dom (g . s) = the
Sorts of
(Free (S,X0)) . s &
rng (i . s) c= the
Sorts of
(Free (S,X0)) . s )
by FUNCT_2:def 1;
then dom ((g . s) * (i . s)) =
dom (i . s)
by RELAT_1:27
.=
the
Sorts of
A0 . s
by FUNCT_2:def 1
;
then A13:
dom (((g . s) * (i . s)) | (G . s)) = G . s
by A12, RELAT_1:62;
the
Sorts of
A0 is
MSSubset of
(Free (S,X0))
by Def6;
then
the
Sorts of
A0 . s c= the
Sorts of
(Free (S,X0)) . s
by PBOOLE:def 2, PBOOLE:def 18;
then
(
G . s c= the
Sorts of
(Free (S,X0)) . s &
dom (g . s) = the
Sorts of
(Free (S,X0)) . s )
by A12, FUNCT_2:def 1;
then A14:
dom ((g . s) | (H . s)) = G . s
by A2, RELAT_1:62;
thus (h || G) . x =
(h . s) | (G . s)
by MSAFREE:def 1
.=
((g . s) * (i . s)) | (G . s)
by MSUALG_3:2
.=
(g . s) | (H . s)
by A13, A14, A15
.=
f . x
by A3, MSAFREE:def 1
;
verum end;
hence
h || G = f
; verum