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;

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

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

consider h1 being ManySortedFunction of A,C such that (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;

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

hence
(g1 || H) . x = (g2 || H) . x
by A31; :: thesis: verum((g1 || H) . p) . y = ((g2 || H) . p) . y

let y be object ; :: thesis: ( y in H . p implies ((g1 || H) . p) . b_{1} = ((g2 || H) . p) . b_{1} )

assume A32: y in H . p ; :: thesis: ((g1 || H) . p) . b_{1} = ((g2 || H) . p) . b_{1}

end;assume A32: y in H . p ; :: thesis: ((g1 || H) . p) . b

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

end;

suppose A33:
( y = t & p = r )
; :: thesis: ((g1 || H) . p) . b_{1} = ((g2 || H) . p) . b_{1}

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;.= 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

suppose A34:
( ( p = r implies y <> t ) & y nin (vf t) . p )
; :: thesis: ((g1 || H) . p) . b_{1} = ((g2 || H) . p) . b_{1}

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;.= (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

suppose A35:
( ( p = r implies y <> t ) & y in (vf t) . p )
; :: thesis: ((g1 || H) . p) . b_{1} = ((g2 || H) . p) . b_{1}

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

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