let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for A being b₁,S -terms MSAlgebra over S holds (canonical_homomorphism A) ** (canonical_homomorphism A) = canonical_homomorphism A
let X be V5() ManySortedSet of S; :: thesis: for A being X,S -terms MSAlgebra over S holds (canonical_homomorphism A) ** (canonical_homomorphism A) = canonical_homomorphism A
let A be X,S -terms MSAlgebra over S; :: thesis: (canonical_homomorphism A) ** (canonical_homomorphism A) = canonical_homomorphism A
set f = canonical_homomorphism A;

now :: thesis: for x being object st x in the carrier of S holds
((canonical_homomorphism A) ** (canonical_homomorphism A)) . x = (canonical_homomorphism A) . x

let x be object ; :: thesis: ( x in the carrier of S implies ((canonical_homomorphism A) ** (canonical_homomorphism A)) . x = (canonical_homomorphism A) . x )
assume x in the carrier of S ; :: thesis: ((canonical_homomorphism A) ** (canonical_homomorphism A)) . x = (canonical_homomorphism A) . x
then reconsider s = x as SortSymbol of S ;
the Sorts of A is MSSubset of (Free (S,X)) by Def6;
then ( the Sorts of A c= the Sorts of (Free (S,X)) & dom ((canonical_homomorphism A) ** (canonical_homomorphism A)) = the carrier of S ) by PARTFUN1:def 2, PBOOLE:def 18;
then A1: ( ((canonical_homomorphism A) ** (canonical_homomorphism A)) . s = ((canonical_homomorphism A) . s) * ((canonical_homomorphism A) . s) & dom ((canonical_homomorphism A) . s) = the Sorts of (Free (S,X)) . s & rng ((canonical_homomorphism A) . s) c= the Sorts of A . s & the Sorts of A . s c= the Sorts of (Free (S,X)) . s ) by PBOOLE:def 19, FUNCT_2:def 1;
then A2: dom (((canonical_homomorphism A) ** (canonical_homomorphism A)) . s) = the Sorts of (Free (S,X)) . s by XBOOLE_1:1, RELAT_1:27;

now :: thesis: for y being object st y in the Sorts of (Free (S,X)) . s holds
(((canonical_homomorphism A) ** (canonical_homomorphism A)) . s) . y = ((canonical_homomorphism A) . s) . y

let y be object ; :: thesis: ( y in the Sorts of (Free (S,X)) . s implies (((canonical_homomorphism A) ** (canonical_homomorphism A)) . s) . y = ((canonical_homomorphism A) . s) . y )
assume A3: y in the Sorts of (Free (S,X)) . s ; :: thesis: (((canonical_homomorphism A) ** (canonical_homomorphism A)) . s) . y = ((canonical_homomorphism A) . s) . y
then A4: ((canonical_homomorphism A) . s) . y in the Sorts of A . s by FUNCT_2:5;
thus (((canonical_homomorphism A) ** (canonical_homomorphism A)) . s) . y = ((canonical_homomorphism A) . s) . (((canonical_homomorphism A) . s) . y) by A1, A3, FUNCT_1:13
.= ((canonical_homomorphism A) . s) . y by A4, Th46 ; :: thesis: verum

end;

hence ((canonical_homomorphism A) ** (canonical_homomorphism A)) . x = (canonical_homomorphism A) . x by A1, A2; :: thesis: verum

end;

hence (canonical_homomorphism A) ** (canonical_homomorphism A) = canonical_homomorphism A ; :: thesis: verum