let h1, h2 be Endomorphism of T; :: thesis: ( (h1 . s) . (x1 -term) = x2 -term & (h1 . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(h1 . s1) . (y -term) = y -term ) & (h2 . s) . (x1 -term) = x2 -term & (h2 . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(h2 . s1) . (y -term) = y -term ) implies h1 = h2 )
assume that
A1: ( (h1 . s) . (x1 -term) = x2 -term & (h1 . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(h1 . s1) . (y -term) = y -term ) ) and
A2: ( (h2 . s) . (x1 -term) = x2 -term & (h2 . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(h2 . s1) . (y -term) = y -term ) ) ; :: thesis: h1 = h2
set s0 = s;
A3: ( h1 is_homomorphism T,T & h2 is_homomorphism T,T ) by MSUALG_6:def 2;
h1 || (FreeGen T) = h2 || (FreeGen T)

proof

let s be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: (h1 || (FreeGen T)) . s = (h2 || (FreeGen T)) . s
thus (h1 || (FreeGen T)) . s = (h2 || (FreeGen T)) . s :: thesis: verum

proof

A6: ( (h1 || (FreeGen T)) . s = (h1 . s) | ((FreeGen T) . s) & (h2 || (FreeGen T)) . s = (h2 . s) | ((FreeGen T) . s) ) by MSAFREE:def 1;
let t be Element of (FreeGen T) . s; :: according to PBOOLE:def 21 :: thesis: ((h1 || (FreeGen T)) . s) . t = ((h2 || (FreeGen T)) . s) . t
t in (FreeGen T) . s ;
then t in FreeGen (s,X) by MSAFREE:def 16;
then consider x being set such that
A5: ( x in X . s & t = root-tree [x,s] ) by MSAFREE:def 15;
reconsider x = x as Element of X . s by A5;
A7: ( ((h1 . s) | ((FreeGen T) . s)) . t = (h1 . s) . t & ((h2 . s) | ((FreeGen T) . s)) . t = (h2 . s) . t ) by FUNCT_1:49;

per cases ( ( x = x1 & s = s ) or ( x = x2 & s = s ) or ( x <> x1 & x <> x2 ) or s <> s ) ;

suppose A9: ( x = x1 & s = s ) ; :: thesis: ((h1 || (FreeGen T)) . s) . t = ((h2 || (FreeGen T)) . s) . t

hence ((h1 || (FreeGen T)) . s) . t = x2 -term by A1, A5, A7, MSAFREE:def 1
.= ((h2 || (FreeGen T)) . s) . t by A2, A5, A7, A9, MSAFREE:def 1 ;
:: thesis: verum

end;

suppose A9: ( x = x2 & s = s ) ; :: thesis: ((h1 || (FreeGen T)) . s) . t = ((h2 || (FreeGen T)) . s) . t

hence ((h1 || (FreeGen T)) . s) . t = x1 -term by A1, A5, A7, MSAFREE:def 1
.= ((h2 || (FreeGen T)) . s) . t by A2, A5, A7, A9, MSAFREE:def 1 ;
:: thesis: verum

end;

suppose A9: ( ( x <> x1 & x <> x2 ) or s <> s ) ; :: thesis: ((h1 || (FreeGen T)) . s) . t = ((h2 || (FreeGen T)) . s) . t

hence ((h1 || (FreeGen T)) . s) . t = x -term by A1, A5, A6, A7
.= ((h2 || (FreeGen T)) . s) . t by A2, A5, A6, A7, A9 ;
:: thesis: verum

end;

end;

end;

end;

hence h1 = h2 by A3, EXTENS_1:19; :: thesis: verum