let S be non empty non void ManySortedSign ; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
let A2 be X,S -terms all_vars_including inheriting_operations MSAlgebra over S; :: thesis:
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 S₁[ 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 S₁[ root-tree [v,s]]

let s be SortSymbol of S; :: thesis:
let v be Element of X . s; :: thesis:
reconsider t = root-tree [v,s] as Term of S,X by MSATERM:4;
let r be SortSymbol of S; :: thesis:
assume A4: root-tree [v,s] in the Sorts of A2 . r ; :: thesis:
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; :: thesis:

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
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]

let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of Sym (o,X); :: thesis:
assume A10: for t being Term of S,X st t in rng p holds
S₁[t] ; :: thesis:
let s be SortSymbol of S; :: thesis:
assume A11: [o, the carrier of S] -tree p in the Sorts of A2 . s ; :: thesis:
( 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;

let i be Nat; :: thesis:
assume A20: i in dom (the_arity_of o) ; :: thesis:
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; :: thesis:

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; :: thesis:

end;

A24: for t being Term of S,X holds S₁[t] from MSATERM:sch 1(A3, A9);
thus canonical_homomorphism A2 is_epimorphism Free (S,X),A2 :: thesis:

thus canonical_homomorphism A2 is_homomorphism Free (S,X),A2 by Def10; :: according to MSUALG_3:def 8 :: thesis:
let x be set ; :: according to MSUALG_3:def 3 :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider s = x as SortSymbol of S ;
thus rng ((canonical_homomorphism A2) . x) c= the Sorts of A2 . x ; :: according to XBOOLE_0:def 10 :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in the Sorts of A2 . x ; :: thesis:
then reconsider t = y as Element of the Sorts of A2 . s ;
t is Term of S,X by Th42;
then A25: ((canonical_homomorphism A2) . s) . t = t by A24;
the Sorts of A2 is MSSubset of (Free (S,X)) by Def6;
then the Sorts of A2 . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def 2, PBOOLE:def 18;
then ( t in the Sorts of (Free (S,X)) . s & dom ((canonical_homomorphism A2) . s) = the Sorts of (Free (S,X)) . s ) by FUNCT_2:def 1;
hence y in proj2 ((canonical_homomorphism A2) . x) by A25, FUNCT_1:def 3; :: thesis:

end;

let s be SortSymbol of S; :: thesis:
let t be Element of the Sorts of A2 . s; :: thesis:
t is Term of S,X by Th42;
hence ((canonical_homomorphism A2) . s) . t = t by A24; :: thesis: