let S be non empty non void ManySortedSign ; :: thesis:
let s be SortSymbol of S; :: thesis:
let X be non-empty ManySortedSet of the carrier of S; :: thesis:
let x, x1 be Element of X . s; :: thesis:
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis:
set H = canonical_homomorphism T;
set h = Hom (T,x,x1);
set g = Hom ((Free (S,X)),x,x1);
defpred S₁[ 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 S₁[x -term ]

let s1 be SortSymbol of S; :: thesis:
let a be Element of X . s1; :: thesis:
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;

suppose C1: ( s = s1 & a = x ) ; :: thesis:

then ( ((Hom ((Free (S,X)),x,x1)) . s1) . (a -term) = x1 -term & ((Hom (T,x,x1)) . s1) . (a -term) = x1 -term ) by HOM;
hence S₁[a -term ] by C1, B3; :: thesis:

end;

suppose C2: ( s = s1 & a = x1 ) ; :: thesis:

then ( ((Hom ((Free (S,X)),x,x1)) . s1) . (a -term) = x -term & ((Hom (T,x,x1)) . s1) . (a -term) = x -term ) by HOM;
hence S₁[a -term ] by C2, B3; :: thesis:

end;

suppose ( s <> s1 or ( a <> x & a <> x1 ) ) ; :: thesis:

then ( ((Hom ((Free (S,X)),x,x1)) . s1) . (a -term) = a -term & ((Hom (T,x,x1)) . s1) . (a -term) = a -term ) by HOM;
hence S₁[a -term ] by B3; :: thesis:

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
S₁[t] ) holds
S₁[o -term p]

let o be OperSymbol of S; :: thesis:
let p be Element of Args (o,(Free (S,X))); :: thesis:
assume Z0: for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ; :: thesis:
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

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 18 :: thesis:
let i be Nat; :: thesis:
assume C0: ( 1 <= i & i <= len (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) # p) ) ; :: thesis:
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:

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:

end;

let s be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis:
thus ((canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1))) . s = ((Hom (T,x,x1)) ** (canonical_homomorphism T)) . s :: thesis:

let t be Element of the Sorts of (Free (S,X)) . s; :: according to PBOOLE:def 21 :: thesis:
A3: S₁[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:

end;