let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: (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; :: thesis: for x being Element of X . s1 holds S1[x -term ]
let a be Element of X . s1; :: thesis: 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 ) ) ;
suppose C1: ( s = s1 & a = x ) ; :: thesis: S1[a -term ]
then ( ((Hom ((Free (S,X)),x,x1)) . s1) . (a -term) = x1 -term & ((Hom (T,x,x1)) . s1) . (a -term) = x1 -term ) by HOM;
hence S1[a -term ] by C1, B3; :: thesis: verum
end;
suppose C2: ( s = s1 & a = x1 ) ; :: thesis: S1[a -term ]
then ( ((Hom ((Free (S,X)),x,x1)) . s1) . (a -term) = x -term & ((Hom (T,x,x1)) . s1) . (a -term) = x -term ) by HOM;
hence S1[a -term ] by C2, B3; :: thesis: verum
end;
suppose ( s <> s1 or ( a <> x & a <> x1 ) ) ; :: thesis: S1[a -term ]
then ( ((Hom ((Free (S,X)),x,x1)) . s1) . (a -term) = a -term & ((Hom (T,x,x1)) . s1) . (a -term) = a -term ) by HOM;
hence S1[a -term ] by B3; :: thesis: verum
end;
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; :: thesis: 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))); :: thesis: ( ( 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] ; :: thesis: 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; :: according to FINSEQ_1:def 17 :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: (((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 ; :: thesis: 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 ; :: thesis: verum
end;
let s be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: ((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 :: thesis: verum
proof
let t be Element of the Sorts of (Free (S,X)) . s; :: according to PBOOLE:def 21 :: thesis: (((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; :: thesis: verum
end;