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
; ( (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
; ( (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
; 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; 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; ( ( 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 ) )
; (h . s1) . (y -term) = y -term
per cases then
( s1 <> s or ( s1 = s & y <> x1 & y <> x2 ) )
;
suppose A7:
(
s1 = s &
y <> x1 &
y <> x2 )
;
(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
;
verum end; end;