let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for A2 being b1,S -terms all_vars_including inheriting_operations MSAlgebra over S holds (canonical_homomorphism A2) ** (canonical_homomorphism A2) = canonical_homomorphism A2
let X be V5() ManySortedSet of S; :: thesis: for A2 being X,S -terms all_vars_including inheriting_operations MSAlgebra over S holds (canonical_homomorphism A2) ** (canonical_homomorphism A2) = canonical_homomorphism A2
let A2 be X,S -terms all_vars_including inheriting_operations MSAlgebra over S; :: thesis: (canonical_homomorphism A2) ** (canonical_homomorphism A2) = canonical_homomorphism A2
set A = A2;
set f = canonical_homomorphism A2;
now :: thesis: for x being object st x in the carrier of S holds
((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . x = (canonical_homomorphism A2) . x
let x be object ; :: thesis: ( x in the carrier of S implies ((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . x = (canonical_homomorphism A2) . x )
assume x in the carrier of S ; :: thesis: ((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . x = (canonical_homomorphism A2) . x
then reconsider s = x as SortSymbol of S ;
the Sorts of A2 is MSSubset of (Free (S,X)) by Def6;
then ( the Sorts of A2 c= the Sorts of (Free (S,X)) & dom ((canonical_homomorphism A2) ** (canonical_homomorphism A2)) = the carrier of S ) by PARTFUN1:def 2, PBOOLE:def 18;
then A1: ( ((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . s = ((canonical_homomorphism A2) . s) * ((canonical_homomorphism A2) . s) & dom ((canonical_homomorphism A2) . s) = the Sorts of (Free (S,X)) . s & rng ((canonical_homomorphism A2) . s) c= the Sorts of A2 . s & the Sorts of A2 . s c= the Sorts of (Free (S,X)) . s ) by PBOOLE:def 19, FUNCT_2:def 1;
then A2: dom (((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . 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 A2) ** (canonical_homomorphism A2)) . s) . y = ((canonical_homomorphism A2) . s) . y
let y be object ; :: thesis: ( y in the Sorts of (Free (S,X)) . s implies (((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . s) . y = ((canonical_homomorphism A2) . s) . y )
assume A3: y in the Sorts of (Free (S,X)) . s ; :: thesis: (((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . s) . y = ((canonical_homomorphism A2) . s) . y
then A4: ((canonical_homomorphism A2) . s) . y in the Sorts of A2 . s by FUNCT_2:5;
thus (((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . s) . y = ((canonical_homomorphism A2) . s) . (((canonical_homomorphism A2) . s) . y) by A1, A3, FUNCT_1:13
.= ((canonical_homomorphism A2) . s) . y by A4, Th47 ; :: thesis: verum
end;
hence ((canonical_homomorphism A2) ** (canonical_homomorphism A2)) . x = (canonical_homomorphism A2) . x by A1, A2; :: thesis: verum
end;
hence (canonical_homomorphism A2) ** (canonical_homomorphism A2) = canonical_homomorphism A2 ; :: thesis: verum