let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being Endomorphism of T st ( for s being SortSymbol of S
for x being Element of X . s holds (h . s) . (x -term) = x -term ) holds
h = id the Sorts of T
let X be V5() ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being Endomorphism of T st ( for s being SortSymbol of S
for x being Element of X . s holds (h . s) . (x -term) = x -term ) holds
h = id the Sorts of T
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for h being Endomorphism of T st ( for s being SortSymbol of S
for x being Element of X . s holds (h . s) . (x -term) = x -term ) holds
h = id the Sorts of T
let h be Endomorphism of T; :: thesis: ( ( for s being SortSymbol of S
for x being Element of X . s holds (h . s) . (x -term) = x -term ) implies h = id the Sorts of T )
A1: id the Sorts of T is_homomorphism T,T by MSUALG_3:9;
A2: h is_homomorphism T,T by MSUALG_6:def 2;
assume Z0: for s being SortSymbol of S
for x being Element of X . s holds (h . s) . (x -term) = x -term ; :: thesis: h = id the Sorts of T
h || (FreeGen T) = (id the Sorts of T) || (FreeGen T)
proof
let s be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: (h || (FreeGen T)) . s = ((id the Sorts of T) || (FreeGen T)) . s
thus (h || (FreeGen T)) . s = ((id the Sorts of T) || (FreeGen T)) . s :: thesis: verum
proof
let t be Element of (FreeGen T) . s; :: according to PBOOLE:def 21 :: thesis: ((h || (FreeGen T)) . s) . t = (((id the Sorts of T) || (FreeGen T)) . s) . t
A6: (FreeGen T) . s c= the Sorts of T . s by PBOOLE:def 2, PBOOLE:def 18;
(FreeGen T) . s = FreeGen (s,X) by MSAFREE:def 16;
then consider x being set such that
A4: ( x in X . s & t = root-tree [x,s] ) by MSAFREE:def 15;
reconsider x = x as Element of X . s by A4;
thus ((h || (FreeGen T)) . s) . t = ((h . s) | ((FreeGen T) . s)) . t by MSAFREE:def 1
.= (h . s) . (x -term) by A4, FUNCT_1:49
.= x -term by Z0
.= (id ( the Sorts of T . s)) . t by A4, A6, FUNCT_1:18
.= ((id the Sorts of T) . s) . t by MSUALG_3:def 1
.= (((id the Sorts of T) . s) | ((FreeGen T) . s)) . t by FUNCT_1:49
.= (((id the Sorts of T) || (FreeGen T)) . s) . t by MSAFREE:def 1 ; :: thesis: verum
end;
end;
hence h = id the Sorts of T by A1, A2, EXTENS_1:19; :: thesis: verum