let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for A2 being b1,S -terms all_vars_including inheriting_operations MSAlgebra over S holds
( canonical_homomorphism A2 is_epimorphism Free (S,X),A2 & ( for s being SortSymbol of S
for t being Element of A2,s holds ((canonical_homomorphism A2) . s) . t = t ) )
let X be V5() ManySortedSet of S; for A2 being X,S -terms all_vars_including inheriting_operations MSAlgebra over S holds
( canonical_homomorphism A2 is_epimorphism Free (S,X),A2 & ( for s being SortSymbol of S
for t being Element of A2,s holds ((canonical_homomorphism A2) . s) . t = t ) )
let A2 be X,S -terms all_vars_including inheriting_operations MSAlgebra over S; ( canonical_homomorphism A2 is_epimorphism Free (S,X),A2 & ( for s being SortSymbol of S
for t being Element of A2,s holds ((canonical_homomorphism A2) . s) . t = t ) )
set A = A2;
A1:
FreeMSA X = Free (S,X)
by MSAFREE3:31;
reconsider G = FreeGen X as GeneratorSet of Free (S,X) by MSAFREE3:31;
set f = canonical_homomorphism A2;
A2:
( canonical_homomorphism A2 is_homomorphism Free (S,X),A2 & (canonical_homomorphism A2) || G = id G )
by Def10;
defpred S1[ set ] means for s being SortSymbol of S st $1 in the Sorts of A2 . s holds
((canonical_homomorphism A2) . s) . $1 = $1;
A3:
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 A2 . r implies ((canonical_homomorphism A2) . r) . (root-tree [v,s]) = root-tree [v,s] )
assume A4:
root-tree [v,s] in the
Sorts of
A2 . r
;
((canonical_homomorphism A2) . r) . (root-tree [v,s]) = root-tree [v,s]
the
Sorts of
A2 is
MSSubset of
(Free (S,X))
by Def6;
then
the
Sorts of
A2 . 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 A4, A1;
then
root-tree [v,s] in FreeSort (
X,
r)
by MSAFREE:def 11;
then A5:
(
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 A6:
root-tree [v,s] in (FreeGen X) . s
by MSAFREE:def 16;
A7:
(id (FreeGen X)) . s = id ((FreeGen X) . s)
by MSUALG_3:def 1;
(((canonical_homomorphism A2) . s) | ((FreeGen X) . s)) . (root-tree [v,s]) = ((canonical_homomorphism A2) . s) . (root-tree [v,s])
by A6, FUNCT_1:49;
then A8:
((canonical_homomorphism A2) . s) . (root-tree [v,s]) =
(id ((FreeGen X) . s)) . (root-tree [v,s])
by A2, A7, MSAFREE:def 1
.=
root-tree [v,s]
by A6, FUNCT_1:18
;
thus
((canonical_homomorphism A2) . r) . (root-tree [v,s]) = root-tree [v,s]
by A5, A8;
verum
end;
A9:
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 A10:
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 A2 . s implies ((canonical_homomorphism A2) . s) . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree p )
assume A11:
[o, the carrier of S] -tree p in the
Sorts of
A2 . s
;
((canonical_homomorphism A2) . 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 A12:
(
(DenOp (o,X)) . p = (Sym (o,X)) -tree p &
(FreeOper X) . o = DenOp (
o,
X) )
by MSAFREE:def 12, MSAFREE:def 13;
A13:
p is
Element of
Args (
o,
(Free (S,X)))
by A1, INSTALG1:1;
reconsider t =
(Sym (o,X)) -tree p as
Term of
S,
X ;
the
Sorts of
A2 is
MSSubset of
(Free (S,X))
by Def6;
then A14:
the
Sorts of
A2 . s c= the
Sorts of
(Free (S,X)) . s
by PBOOLE:def 2, PBOOLE:def 18;
A15:
(
the_sort_of t = the_result_sort_of o &
FreeSort (
X,
s)
= the
Sorts of
(Free (S,X)) . s )
by A1, MSATERM:20, MSAFREE:def 11;
then A16:
s = the_result_sort_of o
by A11, A14, MSATERM:def 5;
A17:
(Den (o,(Free (S,X)))) . p in the
Sorts of
A2 . (the_result_sort_of o)
by A11, A12, A1, A15, A14, MSATERM:def 5;
then A18:
(
p in Args (
o,
A2) &
(Den (o,A2)) . p = (Den (o,(Free (S,X)))) . p )
by A13, Def8;
reconsider q =
p as
Element of
Args (
o,
A2)
by A17, A13, Def8;
reconsider p0 =
p as
Element of
Args (
o,
(Free (S,X)))
by A1, INSTALG1:1;
A19:
(
dom q = dom (the_arity_of o) &
dom ((canonical_homomorphism A2) # p0) = dom (the_arity_of o) &
Args (
o,
A2)
= product ( the Sorts of A2 * (the_arity_of o)) &
dom ( the Sorts of A2 * (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 = ((canonical_homomorphism A2) . ((the_arity_of o) /. i)) . (p0 . i)let i be
Nat;
( i in dom (the_arity_of o) implies q . i = ((canonical_homomorphism A2) . ((the_arity_of o) /. i)) . (p0 . i) )assume A20:
i in dom (the_arity_of o)
;
q . i = ((canonical_homomorphism A2) . ((the_arity_of o) /. i)) . (p0 . i)then A21:
(
(the_arity_of o) /. i = (the_arity_of o) . i &
p0 . i in rng p )
by A19, FUNCT_1:def 3, PARTFUN1:def 6;
A22:
p0 . i in ( the Sorts of A2 * (the_arity_of o)) . i
by A19, A20, CARD_3:9;
then A23:
p0 . i in the
Sorts of
A2 . ((the_arity_of o) . i)
by A20, FUNCT_1:13;
p0 . i is
Element of the
Sorts of
A2 . ((the_arity_of o) /. i)
by A21, A22, A20, FUNCT_1:13;
then
p0 . i is
Term of
S,
X
by Th42;
hence
q . i = ((canonical_homomorphism A2) . ((the_arity_of o) /. i)) . (p0 . i)
by A10, A21, A23;
verum end;
then
(canonical_homomorphism A2) # p0 = q
by A19, MSUALG_3:24;
hence
((canonical_homomorphism A2) . s) . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree p
by A16, A12, A1, A18, Def10, MSUALG_3:def 7;
verum
end;
A24:
for t being Term of S,X holds S1[t]
from MSATERM:sch 1(A3, A9);
thus
canonical_homomorphism A2 is_epimorphism Free (S,X),A2
for s being SortSymbol of S
for t being Element of A2,s holds ((canonical_homomorphism A2) . s) . t = t
let s be SortSymbol of S; for t being Element of A2,s holds ((canonical_homomorphism A2) . s) . t = t
let t be Element of the Sorts of A2 . s; ((canonical_homomorphism A2) . s) . t = t
t is Term of S,X
by Th42;
hence
((canonical_homomorphism A2) . s) . t = t
by A24; verum