let U1, U2 be Universal_Algebra; for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds
h is_homomorphism
let h be Function of U1,U2; ( U1,U2 are_similar & MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_homomorphism )
assume A1:
U1,U2 are_similar
; ( not MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_homomorphism )
A2:
MSSign U1 = MSSign U2
by A1, Th10;
set A = (MSAlg U2) Over (MSSign U1);
set f = MSAlg h;
assume A3:
MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
; h is_homomorphism
thus
U1,U2 are_similar
by A1; ALG_1:def 1 for b1 being set holds
( not b1 in dom the charact of U1 or for b2 being M17( the carrier of U1, Operations U1)
for b3 being M17( the carrier of U2, Operations U2) holds
( not b2 = the charact of U1 . b1 or not b3 = the charact of U2 . b1 or for b4 being FinSequence of the carrier of U1 holds
( not b4 in dom b2 or h . (b2 . b4) = b3 . K138( the carrier of U1, the carrier of U2,b4,h) ) ) )
let n be Nat; ( not n in dom the charact of U1 or for b1 being M17( the carrier of U1, Operations U1)
for b2 being M17( the carrier of U2, Operations U2) holds
( not b1 = the charact of U1 . n or not b2 = the charact of U2 . n or for b3 being FinSequence of the carrier of U1 holds
( not b3 in dom b1 or h . (b1 . b3) = b2 . K138( the carrier of U1, the carrier of U2,b3,h) ) ) )
assume
n in dom the charact of U1
; for b1 being M17( the carrier of U1, Operations U1)
for b2 being M17( the carrier of U2, Operations U2) holds
( not b1 = the charact of U1 . n or not b2 = the charact of U2 . n or for b3 being FinSequence of the carrier of U1 holds
( not b3 in dom b1 or h . (b1 . b3) = b2 . K138( the carrier of U1, the carrier of U2,b3,h) ) )
then reconsider o = n as OperSymbol of (MSSign U1) by Lm3;
let O1 be operation of U1; for b1 being M17( the carrier of U2, Operations U2) holds
( not O1 = the charact of U1 . n or not b1 = the charact of U2 . n or for b2 being FinSequence of the carrier of U1 holds
( not b2 in dom O1 or h . (O1 . b2) = b1 . K138( the carrier of U1, the carrier of U2,b2,h) ) )
let O2 be operation of U2; ( not O1 = the charact of U1 . n or not O2 = the charact of U2 . n or for b1 being FinSequence of the carrier of U1 holds
( not b1 in dom O1 or h . (O1 . b1) = O2 . K138( the carrier of U1, the carrier of U2,b1,h) ) )
assume that
A4:
O1 = the charact of U1 . n
and
A5:
O2 = the charact of U2 . n
; for b1 being FinSequence of the carrier of U1 holds
( not b1 in dom O1 or h . (O1 . b1) = O2 . K138( the carrier of U1, the carrier of U2,b1,h) )
A6:
O1 = Den (o,(MSAlg U1))
by A4, Th12;
let x be FinSequence of U1; ( not x in dom O1 or h . (O1 . x) = O2 . K138( the carrier of U1, the carrier of U2,x,h) )
assume
x in dom O1
; h . (O1 . x) = O2 . K138( the carrier of U1, the carrier of U2,x,h)
then reconsider y = x as Element of Args (o,(MSAlg U1)) by A6, FUNCT_2:def 1;
A7:
((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = h . (O1 . y)
by A1, A6, Th11;
A8:
((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y)
by A3;
A9:
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #)
by MSUALG_1:def 11;
Den (o,((MSAlg U2) Over (MSSign U1))) =
the Charact of ((MSAlg U2) Over (MSSign U1)) . o
by MSUALG_1:def 6
.=
(MSCharact U2) . o
by A2, A9, Th9
.=
O2
by A5, MSUALG_1:def 10
;
hence
h . (O1 . x) = O2 . K138( the carrier of U1, the carrier of U2,x,h)
by A1, A7, A8, Th15; verum