let w1, w2 be Element of C -States the generators of G; ( (w1 . r) . t = v & ( for p being SortSymbol of S
for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (w1 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds
for q being Element of A,p st q = ((supp-term t) . p) . x holds
(w1 . p) . x = q value_at (C,u) ) ) ) & (w2 . r) . t = v & ( for p being SortSymbol of S
for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (w2 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds
for q being Element of A,p st q = ((supp-term t) . p) . x holds
(w2 . p) . x = q value_at (C,u) ) ) ) implies w1 = w2 )
assume that
A28:
( (w1 . r) . t = v & ( for p being SortSymbol of S
for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (w1 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds
for q being Element of A,p st q = ((supp-term t) . p) . x holds
(w1 . p) . x = q value_at (C,u) ) ) ) )
and
A29:
( (w2 . r) . t = v & ( for p being SortSymbol of S
for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (w2 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds
for q being Element of A,p st q = ((supp-term t) . p) . x holds
(w2 . p) . x = q value_at (C,u) ) ) ) )
; w1 = w2
reconsider g1 = w1, g2 = w2 as ManySortedFunction of the generators of G, the Sorts of C by Th43;
reconsider H = FreeGen X as ManySortedSubset of the generators of G by A1;
A30:
now for x being object st x in the carrier of S holds
(g1 || H) . x = (g2 || H) . xlet x be
object ;
( x in the carrier of S implies (g1 || H) . x = (g2 || H) . x )assume
x in the
carrier of
S
;
(g1 || H) . x = (g2 || H) . xthen reconsider p =
x as
SortSymbol of
S ;
A31:
(
dom ((g1 || H) . p) = H . p &
dom ((g2 || H) . p) = H . p )
by FUNCT_2:def 1;
now for y being object st y in H . p holds
((g1 || H) . p) . y = ((g2 || H) . p) . ylet y be
object ;
( y in H . p implies ((g1 || H) . p) . b1 = ((g2 || H) . p) . b1 )assume A32:
y in H . p
;
((g1 || H) . p) . b1 = ((g2 || H) . p) . b1per cases
( ( y = t & p = r ) or ( ( p = r implies y <> t ) & y nin (vf t) . p ) or ( ( p = r implies y <> t ) & y in (vf t) . p ) )
;
suppose A35:
( (
p = r implies
y <> t ) &
y in (vf t) . p )
;
((g1 || H) . p) . b1 = ((g2 || H) . p) . b1reconsider q =
((supp-term t) . p) . y as
Element of
A,
p by A35, FUNCT_2:5;
reconsider f =
s as
ManySortedFunction of the
generators of
G, the
Sorts of
C by Th43;
reconsider u =
(f || H) +* (
r,
(supp-var t),
v) as
ManySortedFunction of
FreeGen X, the
Sorts of
C ;
thus ((g1 || H) . p) . y =
((g1 . p) | (H . p)) . y
by MSAFREE:def 1
.=
(g1 . p) . y
by A32, FUNCT_1:49
.=
q value_at (
C,
u)
by A28, A35, A32
.=
(w2 . p) . y
by A29, A35, A32
.=
((g2 . p) | (H . p)) . y
by A32, FUNCT_1:49
.=
((g2 || H) . p) . y
by MSAFREE:def 1
;
verum end; end; end; hence
(g1 || H) . x = (g2 || H) . x
by A31;
verum end;
consider h1 being ManySortedFunction of A,C such that
A36:
( h1 is_homomorphism A,C & g1 = h1 || the generators of G )
by Def18;
consider h2 being ManySortedFunction of A,C such that
A37:
( h2 is_homomorphism A,C & g2 = h2 || the generators of G )
by Def18;
reconsider I = H as GeneratorSet of A by MSAFREE4:45;
( h1 || I = g1 || H & h2 || I = g2 || H )
by A36, A37, EQUATION:5;
hence
w1 = w2
by A30, A36, A37, EXTENS_1:19, PBOOLE:3; verum