let S be non empty non void ManySortedSign ; for X being non-empty ManySortedSet of S
for A being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A is Free (S,X) -Image
let X be non-empty ManySortedSet of S; for A being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A is Free (S,X) -Image
let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; A is Free (S,X) -Image
now ex B being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S ex f0 being ManySortedFunction of (Free (S,X)),B st
( f0 is_homomorphism Free (S,X),B & MSAlgebra(# the Sorts of A, the Charact of A #) = Image f0 )take B =
A;
ex f0 being ManySortedFunction of (Free (S,X)),B st
( f0 is_homomorphism Free (S,X),B & MSAlgebra(# the Sorts of A, the Charact of A #) = Image f0 )
FreeGen X is
ManySortedSubset of the
Sorts of
A
by Def7;
then
(
FreeGen X is
free &
id (FreeGen X) is
ManySortedFunction of
FreeGen X, the
Sorts of
A )
by Th22;
then consider f being
ManySortedFunction of
(FreeMSA X),
A such that A1:
(
f is_homomorphism FreeMSA X,
A &
f || (FreeGen X) = id (FreeGen X) )
;
A2:
Free (
S,
X)
= FreeMSA X
by MSAFREE3:31;
reconsider f0 =
f as
ManySortedFunction of
(Free (S,X)),
B by MSAFREE3:31;
take f0 =
f0;
( f0 is_homomorphism Free (S,X),B & MSAlgebra(# the Sorts of A, the Charact of A #) = Image f0 )thus A3:
f0 is_homomorphism Free (
S,
X),
B
by A1, MSAFREE3:31;
MSAlgebra(# the Sorts of A, the Charact of A #) = Image f0reconsider C =
MSAlgebra(# the
Sorts of
B, the
Charact of
B #) as
strict non-empty MSSubAlgebra of
A by MSUALG_2:5;
the
Sorts of
C = f0 .:.: the
Sorts of
(Free (S,X))
proof
defpred S1[
set ]
means for
s being
SortSymbol of
S st $1
in the
Sorts of
C . s holds
( $1
in (f0 .:.: the Sorts of (Free (S,X))) . s &
(f0 . s) . $1
= $1 );
A4:
for
s being
SortSymbol of
S for
v being
Element of
X . s holds
S1[
root-tree [v,s]]
proof
let s be
SortSymbol of
S;
for v being Element of X . s holds S1[ root-tree [v,s]]let v be
Element of
X . s;
S1[ root-tree [v,s]]
reconsider t =
root-tree [v,s] as
Term of
S,
X by MSATERM:4;
let r be
SortSymbol of
S;
( root-tree [v,s] in the Sorts of C . r implies ( root-tree [v,s] in (f0 .:.: the Sorts of (Free (S,X))) . r & (f0 . r) . (root-tree [v,s]) = root-tree [v,s] ) )
assume A5:
root-tree [v,s] in the
Sorts of
C . r
;
( root-tree [v,s] in (f0 .:.: the Sorts of (Free (S,X))) . r & (f0 . r) . (root-tree [v,s]) = root-tree [v,s] )
the
Sorts of
C is
MSSubset of
(Free (S,X))
by Def6;
then
the
Sorts of
C . r c= the
Sorts of
(Free (S,X)) . r
by PBOOLE:def 2, PBOOLE:def 18;
then
root-tree [v,s] in (FreeSort X) . r
by A5, A2;
then
root-tree [v,s] in FreeSort (
X,
r)
by MSAFREE:def 11;
then A6:
(
the_sort_of t = r &
s = the_sort_of t )
by MSATERM:def 5, MSATERM:14;
root-tree [v,s] in FreeGen (
s,
X)
by MSAFREE:def 15;
then A7:
root-tree [v,s] in (FreeGen X) . s
by MSAFREE:def 16;
A8:
(f0 .:.: the Sorts of (Free (S,X))) . s = (f0 . s) .: ( the Sorts of (Free (S,X)) . s)
by PBOOLE:def 20;
A9:
(id (FreeGen X)) . s = id ((FreeGen X) . s)
by MSUALG_3:def 1;
((f . s) | ((FreeGen X) . s)) . (root-tree [v,s]) = (f . s) . (root-tree [v,s])
by A7, FUNCT_1:49;
then A10:
(f . s) . (root-tree [v,s]) =
(id ((FreeGen X) . s)) . (root-tree [v,s])
by A1, A9, MSAFREE:def 1
.=
root-tree [v,s]
by A7, FUNCT_1:18
;
FreeGen X is
MSSubset of
(Free (S,X))
by MSAFREE3:31;
then
(
(FreeGen X) . s c= the
Sorts of
(Free (S,X)) . s &
dom (f0 . s) = the
Sorts of
(Free (S,X)) . s )
by FUNCT_2:def 1, PBOOLE:def 2, PBOOLE:def 18;
hence
(
root-tree [v,s] in (f0 .:.: the Sorts of (Free (S,X))) . r &
(f0 . r) . (root-tree [v,s]) = root-tree [v,s] )
by A6, A8, A7, A10, FUNCT_1:def 6;
verum
end;
A11:
for
o being
OperSymbol of
S for
p being
ArgumentSeq of
Sym (
o,
X) st ( for
t being
Term of
S,
X st
t in rng p holds
S1[
t] ) holds
S1[
[o, the carrier of S] -tree p]
proof
let o be
OperSymbol of
S;
for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]let p be
ArgumentSeq of
Sym (
o,
X);
( ( for t being Term of S,X st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A12:
for
t being
Term of
S,
X st
t in rng p holds
S1[
t]
;
S1[[o, the carrier of S] -tree p]
let s be
SortSymbol of
S;
( [o, the carrier of S] -tree p in the Sorts of C . s implies ( [o, the carrier of S] -tree p in (f0 .:.: the Sorts of (Free (S,X))) . s & (f0 . s) . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree p ) )
assume A13:
[o, the carrier of S] -tree p in the
Sorts of
C . s
;
( [o, the carrier of S] -tree p in (f0 .:.: the Sorts of (Free (S,X))) . s & (f0 . s) . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree p )
(
Sym (
o,
X)
==> roots p &
p is
FinSequence of
TS (DTConMSA X) )
by MSATERM:def 1, MSATERM:21;
then A14:
(
(DenOp (o,X)) . p = (Sym (o,X)) -tree p &
(FreeOper X) . o = DenOp (
o,
X) )
by MSAFREE:def 12, MSAFREE:def 13;
A15:
p is
Element of
Args (
o,
(Free (S,X)))
by A2, INSTALG1:1;
reconsider t =
(Sym (o,X)) -tree p as
Term of
S,
X ;
the
Sorts of
C is
MSSubset of
(Free (S,X))
by Def6;
then A16:
the
Sorts of
C . s c= the
Sorts of
(Free (S,X)) . s
by PBOOLE:def 2, PBOOLE:def 18;
A17:
(
the_sort_of t = the_result_sort_of o &
FreeSort (
X,
s)
= the
Sorts of
(Free (S,X)) . s )
by A2, MSATERM:20, MSAFREE:def 11;
then A18:
s = the_result_sort_of o
by A13, A16, MSATERM:def 5;
A19:
(Den (o,(Free (S,X)))) . p in the
Sorts of
A . (the_result_sort_of o)
by A13, A14, A2, A17, A16, MSATERM:def 5;
then A20:
(
p in Args (
o,
A) &
(Den (o,A)) . p = (Den (o,(Free (S,X)))) . p )
by A15, Def8;
reconsider q =
p as
Element of
Args (
o,
A)
by A19, A15, Def8;
reconsider p0 =
p as
Element of
Args (
o,
(Free (S,X)))
by A2, INSTALG1:1;
A21:
(
dom q = dom (the_arity_of o) &
dom (f0 # p0) = dom (the_arity_of o) &
Args (
o,
A)
= product ( the Sorts of A * (the_arity_of o)) &
dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) )
by MSUALG_3:6, PRALG_2:3;
now for i being Nat st i in dom (the_arity_of o) holds
q . i = (f0 . ((the_arity_of o) /. i)) . (p0 . i)let i be
Nat;
( i in dom (the_arity_of o) implies q . i = (f0 . ((the_arity_of o) /. i)) . (p0 . i) )assume A22:
i in dom (the_arity_of o)
;
q . i = (f0 . ((the_arity_of o) /. i)) . (p0 . i)then A23:
(
(the_arity_of o) /. i = (the_arity_of o) . i &
p0 . i in rng p )
by A21, FUNCT_1:def 3, PARTFUN1:def 6;
A24:
p0 . i in ( the Sorts of A * (the_arity_of o)) . i
by A21, A22, CARD_3:9;
then A25:
p0 . i in the
Sorts of
A . ((the_arity_of o) . i)
by A22, FUNCT_1:13;
p0 . i is
Element of the
Sorts of
A . ((the_arity_of o) /. i)
by A23, A24, A22, FUNCT_1:13;
then
p0 . i is
Term of
S,
X
by Th42;
hence
q . i = (f0 . ((the_arity_of o) /. i)) . (p0 . i)
by A12, A23, A25;
verum end;
then A26:
f0 # p0 = q
by A21, MSUALG_3:24;
then A27:
(f0 . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . p) = (Den (o,A)) . p
by A3;
A28:
(f0 .:.: the Sorts of (Free (S,X))) . s = (f0 . s) .: ( the Sorts of (Free (S,X)) . s)
by PBOOLE:def 20;
(
dom (f0 . s) = the
Sorts of
(Free (S,X)) . s &
[o, the carrier of S] -tree p in the
Sorts of
(Free (S,X)) . s &
(f0 . s) . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree p )
by A14, A2, A16, A27, A18, A13, A15, Def8, FUNCT_2:def 1;
hence
[o, the carrier of S] -tree p in (f0 .:.: the Sorts of (Free (S,X))) . s
by A28, FUNCT_1:def 6;
(f0 . s) . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree p
thus
(f0 . s) . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree p
by A18, A14, A2, A20, A26, A1;
verum
end;
A29:
for
t being
Term of
S,
X holds
S1[
t]
from MSATERM:sch 1(A4, A11);
hence
the
Sorts of
C = f0 .:.: the
Sorts of
(Free (S,X))
by PBOOLE:146;
verum
end; hence
MSAlgebra(# the
Sorts of
A, the
Charact of
A #)
= Image f0
by A3, MSUALG_3:def 12;
verum end;
hence
A is Free (S,X) -Image
; verum