let w1, w2 be Element of C -States the generators of G; :: thesis: ( (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) ) ) ) ) ; :: thesis: 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 :: thesis: for x being object st x in the carrier of S holds
(g1 || H) . x = (g2 || H) . x
let x be object ; :: thesis: ( x in the carrier of S implies (g1 || H) . x = (g2 || H) . x )
assume x in the carrier of S ; :: thesis: (g1 || H) . x = (g2 || H) . x
then 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 :: thesis: for y being object st y in H . p holds
((g1 || H) . p) . y = ((g2 || H) . p) . y
let y be object ; :: thesis: ( y in H . p implies ((g1 || H) . p) . b1 = ((g2 || H) . p) . b1 )
assume A32: y in H . p ; :: thesis: ((g1 || H) . p) . b1 = ((g2 || H) . p) . b1
per 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 A33: ( y = t & p = r ) ; :: thesis: ((g1 || H) . p) . b1 = ((g2 || H) . p) . b1
thus ((g1 || H) . p) . y = ((g1 . p) | (H . p)) . y by MSAFREE:def 1
.= v by A28, A33, A32, FUNCT_1:49
.= ((g2 . p) | (H . p)) . y by A29, A33, A32, FUNCT_1:49
.= ((g2 || H) . p) . y by MSAFREE:def 1 ; :: thesis: verum
end;
suppose A34: ( ( p = r implies y <> t ) & y nin (vf t) . p ) ; :: thesis: ((g1 || H) . p) . b1 = ((g2 || H) . p) . b1
thus ((g1 || H) . p) . y = ((g1 . p) | (H . p)) . y by MSAFREE:def 1
.= (g1 . p) . y by A32, FUNCT_1:49
.= (s . p) . y by A28, A34, A32
.= (g2 . p) . y by A29, A34, A32
.= ((g2 . p) | (H . p)) . y by A32, FUNCT_1:49
.= ((g2 || H) . p) . y by MSAFREE:def 1 ; :: thesis: verum
end;
suppose A35: ( ( p = r implies y <> t ) & y in (vf t) . p ) ; :: thesis: ((g1 || H) . p) . b1 = ((g2 || H) . p) . b1
reconsider 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 ; :: thesis: verum
end;
end;
end;
hence (g1 || H) . x = (g2 || H) . x by A31; :: thesis: 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; :: thesis: verum