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)); ( 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)]
; G1 = G2
set H1 = G1;
set H2 = G2;
A1 = (FreeMSA X) | (S1,f,g)
;
hence
G1 = G2
by A5, A7, A9, EXTENS_1:14, PBOOLE:3; verum