let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x, x1 being Element of X . s
for T being b2,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds (canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) ** (canonical_homomorphism T)
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x, x1 being Element of X . s
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds (canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) ** (canonical_homomorphism T)
let X be V5() ManySortedSet of the carrier of S; for x, x1 being Element of X . s
for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds (canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) ** (canonical_homomorphism T)
let x, x1 be Element of X . s; for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds (canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) ** (canonical_homomorphism T)
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; (canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) ** (canonical_homomorphism T)
set H = canonical_homomorphism T;
set h = Hom (T,x,x1);
set g = Hom ((Free (S,X)),x,x1);
defpred S1[ Element of (Free (S,X))] means ((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . $1 = ((Hom (T,x,x1)) ** (canonical_homomorphism T)) . $1;
A1:
for s being SortSymbol of S
for x being Element of X . s holds S1[x -term ]
proof
let s1 be
SortSymbol of
S;
for x being Element of X . s1 holds S1[x -term ]let a be
Element of
X . s1;
S1[a -term ]
set r =
a -term ;
the_sort_of (a -term) = s1
by SORT;
then B1:
(
((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . (a -term) = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s1) . (a -term) &
((Hom (T,x,x1)) ** (canonical_homomorphism T)) . (a -term) = (((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s1) . (a -term) &
(canonical_homomorphism T) . (a -term) = ((canonical_homomorphism T) . s1) . (a -term) )
by ABBR;
B2:
(
((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s1 = ((canonical_homomorphism T) . s1) * ((Hom ((Free (S,X)),x,x1)) . s1) &
((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s1 = ((Hom (T,x,x1)) . s1) * ((canonical_homomorphism T) . s1) )
by MSUALG_3:2;
B3:
(
((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . (a -term) = ((canonical_homomorphism T) . s1) . (((Hom ((Free (S,X)),x,x1)) . s1) . (a -term)) &
((Hom (T,x,x1)) ** (canonical_homomorphism T)) . (a -term) = ((Hom (T,x,x1)) . s1) . (((canonical_homomorphism T) . s1) . (a -term)) )
by B1, B2, FUNCT_2:15;
per cases
( ( s = s1 & a = x ) or ( s = s1 & a = x1 ) or s <> s1 or ( a <> x & a <> x1 ) )
;
end;
end;
A2:
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]
proof
let o be
OperSymbol of
S;
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]let p be
Element of
Args (
o,
(Free (S,X)));
( ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) implies S1[o -term p] )
assume Z0:
for
t being
Element of
(Free (S,X)) st
t in rng p holds
S1[
t]
;
S1[o -term p]
A4:
(Den (o,(Free (S,X)))) . p = o -term p
by MSAFREE4:13;
set q =
o -term p;
set r =
the_sort_of (o -term p);
A5:
the_sort_of (o -term p) = the_result_sort_of o
by Th8;
A10:
(
Hom (
(Free (S,X)),
x,
x1)
is_homomorphism Free (
S,
X),
Free (
S,
X) &
Hom (
T,
x,
x1)
is_homomorphism T,
T &
canonical_homomorphism T is_homomorphism Free (
S,
X),
T )
by MSUALG_6:def 2, MSAFREE4:def 10;
A8:
((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p = ((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p
proof
A9:
(
dom (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) = dom (the_arity_of o) &
dom (the_arity_of o) = dom (((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p) )
by MSUALG_3:6;
hence
len (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) = len (((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p)
by FINSEQ_3:29;
FINSEQ_1:def 17 for b1 being set holds
( not 1 <= b1 or not b1 <= len (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) or (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) . b1 = (((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p) . b1 )
let i be
Nat;
( not 1 <= i or not i <= len (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) or (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) . i = (((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p) . i )
assume C0:
( 1
<= i &
i <= len (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) )
;
(((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) . i = (((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p) . i
then C1:
i in dom (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p)
by FINSEQ_3:25;
C3:
dom p = dom (the_arity_of o)
by MSUALG_6:2;
then C5:
(
p /. i = p . i &
p . i in the
Sorts of
(Free (S,X)) . ((the_arity_of o) /. i) )
by C0, A9, FINSEQ_3:25, PARTFUN1:def 6, MSUALG_6:2;
then C4:
(
the_sort_of (p /. i) = (the_arity_of o) /. i &
p . i in rng p )
by A9, C1, C3, SORT, FUNCT_1:def 3;
thus (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) . i =
(((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . ((the_arity_of o) /. i)) . (p /. i)
by C0, C3, C5, A9, FINSEQ_3:25, MSUALG_3:def 6
.=
((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . (p /. i)
by C4, ABBR
.=
((Hom (T,x,x1)) ** (canonical_homomorphism T)) . (p /. i)
by Z0, C4, C5
.=
(((Hom (T,x,x1)) ** (canonical_homomorphism T)) . ((the_arity_of o) /. i)) . (p /. i)
by C4, ABBR
.=
(((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p) . i
by C0, C3, C5, A9, FINSEQ_3:25, MSUALG_3:def 6
;
verum
end;
thus ((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . (o -term p) =
(((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . (the_sort_of (o -term p))) . (o -term p)
by ABBR
.=
(Den (o,T)) . (((Hom (T,x,x1)) ** (canonical_homomorphism T)) # p)
by A8, A4, A5, A10, MSUALG_3:10, MSUALG_3:def 7
.=
(((Hom (T,x,x1)) ** (canonical_homomorphism T)) . (the_sort_of (o -term p))) . (o -term p)
by A4, A5, A10, MSUALG_3:10, MSUALG_3:def 7
.=
((Hom (T,x,x1)) ** (canonical_homomorphism T)) . (o -term p)
by ABBR
;
verum
end;
let s be SortSymbol of S; PBOOLE:def 21 ((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s = ((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s
thus
((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s = ((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s
verumproof
let t be
Element of the
Sorts of
(Free (S,X)) . s;
PBOOLE:def 21 (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s) . t = (((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s) . t
A3:
S1[
t]
from MSAFREE5:sch 2(A1, A2);
the_sort_of t = s
by SORT;
then
(
((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . t = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s) . t &
((Hom (T,x,x1)) ** (canonical_homomorphism T)) . t = (((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s) . t )
by ABBR;
hence
(((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s) . t = (((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s) . t
by A3;
verum
end;