let h1, h2 be Endomorphism of T; :: thesis:
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:
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)

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

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:

end;

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:

end;

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:

end;