reconsider y1 = x1 -term , y2 = x2 -term as Element of (FreeGen T) . s by Th119;
set f = (id (FreeGen T)) +* (s,(((id (FreeGen T)) . s) +* (y1 <-> y2)));
A8: dom (id (FreeGen T)) = the carrier of S by PARTFUN1:def 2;
then A5: ((id (FreeGen T)) +* (s,(((id (FreeGen T)) . s) +* (y1 <-> y2)))) . s = ((id (FreeGen T)) . s) +* (y1 <-> y2) by FUNCT_7:31;
A6: ( dom (y1 <-> y2) = {y1,y2} & y1 in {y1,y2} & y2 in {y1,y2} ) by LemS, TARSKI:def 2;
( (id (FreeGen T)) +* (s,(((id (FreeGen T)) . s) +* (y1 <-> y2))) is ManySortedFunction of FreeGen T, the Sorts of T & FreeGen X = FreeGen T ) by MSAFREE4:22;
then consider h being ManySortedFunction of T,T such that
A1: ( h is_homomorphism T,T & h || (FreeGen T) = (id (FreeGen T)) +* (s,(((id (FreeGen T)) . s) +* (y1 <-> y2))) ) by MSAFREE4:def 9;
reconsider h = h as Endomorphism of T by A1, MSUALG_6:def 2;
take h ; :: thesis: ( (h . s) . (x1 -term) = x2 -term & (h . 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
(h . s1) . (y -term) = y -term ) )
thus (h . s) . (x1 -term) = ((h . s) | ((FreeGen T) . s)) . (x1 -term) by Th119, FUNCT_1:49
.= ((h || (FreeGen T)) . s) . (x1 -term) by MSAFREE:def 1
.= (y1 <-> y2) . y1 by A1, A5, A6, FUNCT_4:13
.= x2 -term by LemS ; :: thesis: ( (h . 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
(h . s1) . (y -term) = y -term ) )
thus (h . s) . (x2 -term) = ((h . s) | ((FreeGen T) . s)) . (x2 -term) by Th119, FUNCT_1:49
.= ((h || (FreeGen T)) . s) . (x2 -term) by MSAFREE:def 1
.= (y1 <-> y2) . y2 by A1, A5, A6, FUNCT_4:13
.= x1 -term by LemS ; :: thesis: for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(h . s1) . (y -term) = y -term
let s1 be SortSymbol of S; :: thesis: for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(h . s1) . (y -term) = y -term
let y be Element of X . s1; :: thesis: ( ( s1 <> s or ( y <> x1 & y <> x2 ) ) implies (h . s1) . (y -term) = y -term )
B5: y -term in (FreeGen T) . s1 by Th119;
B6: (h . s1) . (y -term) = ((h . s1) | ((FreeGen T) . s1)) . (y -term) by Th119, FUNCT_1:49
.= ((h || (FreeGen T)) . s1) . (y -term) by MSAFREE:def 1 ;
assume ( s1 <> s or ( y <> x1 & y <> x2 ) ) ; :: thesis: (h . s1) . (y -term) = y -term
per cases then ( s1 <> s or ( s1 = s & y <> x1 & y <> x2 ) ) ;
suppose s1 <> s ; :: thesis: (h . s1) . (y -term) = y -term
hence (h . s1) . (y -term) = ((id (FreeGen T)) . s1) . (y -term) by A1, B6, FUNCT_7:32
.= (id ((FreeGen T) . s1)) . (y -term) by MSUALG_3:def 1
.= y -term by B5, FUNCT_1:17 ;
:: thesis: verum
end;
suppose A7: ( s1 = s & y <> x1 & y <> x2 ) ; :: thesis: (h . s1) . (y -term) = y -term
then ( [y,s1] <> [x1,s] & [y,s1] <> [x2,s] ) by XTUPLE_0:1;
then ( y -term <> x1 -term & y -term <> x2 -term ) by TREES_4:4;
then A9: y -term nin {y1,y2} by TARSKI:def 2;
thus (h . s1) . (y -term) = (((id (FreeGen T)) . s1) +* (y1 <-> y2)) . (y -term) by A1, A8, B6, A7, FUNCT_7:31
.= ((id (FreeGen T)) . s1) . (y -term) by A6, A9, FUNCT_4:11
.= (id ((FreeGen T) . s1)) . (y -term) by MSUALG_3:def 1
.= y -term by B5, FUNCT_1:17 ; :: thesis: verum
end;
end;