reconsider A1 = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by A1, Th22;

let G1, G2 be ManySortedFunction of the Sorts of (FreeMSA (X * f)), the Sorts of ((FreeMSA X) | (S1,f,g)); :: thesis: ( G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) implies G1 = G2 )

assume that

A5: G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and

A6: for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] and

A7: G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and

A8: for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ; :: thesis: G1 = G2

set H1 = G1;

set H2 = G2;

hence G1 = G2 by A5, A7, A9, EXTENS_1:14, PBOOLE:3; :: thesis: verum

let G1, G2 be ManySortedFunction of the Sorts of (FreeMSA (X * f)), the Sorts of ((FreeMSA X) | (S1,f,g)); :: thesis: ( G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) implies G1 = G2 )

assume that

A5: G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and

A6: for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] and

A7: G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and

A8: for s being SortSymbol of S1

for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ; :: thesis: G1 = G2

set H1 = G1;

set H2 = G2;

A9: now :: thesis: for x being object st x in the carrier of S1 holds

(G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x

A1 = (FreeMSA X) | (S1,f,g)
;(G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x

let x be object ; :: thesis: ( x in the carrier of S1 implies (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x )

assume x in the carrier of S1 ; :: thesis: (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x

then reconsider s = x as SortSymbol of S1 ;

reconsider g1 = (G1 || (FreeGen (X * f))) . s, g2 = (G2 || (FreeGen (X * f))) . s as Function of ((FreeGen (X * f)) . s),( the Sorts of A1 . s) ;

end;assume x in the carrier of S1 ; :: thesis: (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x

then reconsider s = x as SortSymbol of S1 ;

reconsider g1 = (G1 || (FreeGen (X * f))) . s, g2 = (G2 || (FreeGen (X * f))) . s as Function of ((FreeGen (X * f)) . s),( the Sorts of A1 . s) ;

now :: thesis: for z being Element of (FreeGen (X * f)) . s holds g1 . z = g2 . z

hence
(G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x
by FUNCT_2:63; :: thesis: verumlet z be Element of (FreeGen (X * f)) . s; :: thesis: g1 . z = g2 . z

FreeGen (s,(X * f)) = (FreeGen (X * f)) . s by MSAFREE:def 16;

then consider a being set such that

A10: a in (X * f) . s and

A11: z = root-tree [a,s] by MSAFREE:def 15;

reconsider a = a as Element of (X * f) . s by A10;

thus g1 . z = (G1 . s) . z by Th39

.= root-tree [a,(f . s)] by A6, A11

.= (G2 . s) . z by A8, A11

.= g2 . z by Th39 ; :: thesis: verum

end;FreeGen (s,(X * f)) = (FreeGen (X * f)) . s by MSAFREE:def 16;

then consider a being set such that

A10: a in (X * f) . s and

A11: z = root-tree [a,s] by MSAFREE:def 15;

reconsider a = a as Element of (X * f) . s by A10;

thus g1 . z = (G1 . s) . z by Th39

.= root-tree [a,(f . s)] by A6, A11

.= (G2 . s) . z by A8, A11

.= g2 . z by Th39 ; :: thesis: verum

hence G1 = G2 by A5, A7, A9, EXTENS_1:14, PBOOLE:3; :: thesis: verum