let U1, U2 be Universal_Algebra; :: thesis: 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 U1,U2
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar & MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_homomorphism U1,U2 )
assume A1: U1,U2 are_similar ; :: thesis: ( not MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_homomorphism U1,U2 )
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) ; :: thesis: h is_homomorphism U1,U2
thus U1,U2 are_similar by A1; :: according to ALG_1:def 1 :: thesis: for b₁ being Element of NAT holds
( not b₁ in dom the charact of U1 or for b₂ being M16(the carrier of U1, Operations U1)
for b₃ being M16(the carrier of U2, Operations U2) holds
( not b₂ = the charact of U1 . b₁ or not b₃ = the charact of U2 . b₁ or for b₄ being FinSequence of the carrier of U1 holds
( not b₄ in dom b₂ or h . (b₂ . b₄) = b₃ . K156(the carrier of U1,the carrier of U2,b₄,h) ) ) )
let n be Element of NAT ; :: thesis: ( not n in dom the charact of U1 or for b₁ being M16(the carrier of U1, Operations U1)
for b₂ being M16(the carrier of U2, Operations U2) holds
( not b₁ = the charact of U1 . n or not b₂ = the charact of U2 . n or for b₃ being FinSequence of the carrier of U1 holds
( not b₃ in dom b₁ or h . (b₁ . b₃) = b₂ . K156(the carrier of U1,the carrier of U2,b₃,h) ) ) )
assume n in dom the charact of U1 ; :: thesis: for b₁ being M16(the carrier of U1, Operations U1)
for b₂ being M16(the carrier of U2, Operations U2) holds
( not b₁ = the charact of U1 . n or not b₂ = the charact of U2 . n or for b₃ being FinSequence of the carrier of U1 holds
( not b₃ in dom b₁ or h . (b₁ . b₃) = b₂ . K156(the carrier of U1,the carrier of U2,b₃,h) ) )
then reconsider o = n as OperSymbol of (MSSign U1) by Lm3;
let O1 be operation of U1; :: thesis: for b₁ being M16(the carrier of U2, Operations U2) holds
( not O1 = the charact of U1 . n or not b₁ = the charact of U2 . n or for b₂ being FinSequence of the carrier of U1 holds
( not b₂ in dom O1 or h . (O1 . b₂) = b₁ . K156(the carrier of U1,the carrier of U2,b₂,h) ) )
let O2 be operation of U2; :: thesis: ( not O1 = the charact of U1 . n or not O2 = the charact of U2 . n or for b₁ being FinSequence of the carrier of U1 holds
( not b₁ in dom O1 or h . (O1 . b₁) = O2 . K156(the carrier of U1,the carrier of U2,b₁,h) ) )
assume that
A4: O1 = the charact of U1 . n and
A5: O2 = the charact of U2 . n ; :: thesis: for b₁ being FinSequence of the carrier of U1 holds
( not b₁ in dom O1 or h . (O1 . b₁) = O2 . K156(the carrier of U1,the carrier of U2,b₁,h) )
A6: O1 = Den o,(MSAlg U1) by A4, Th12;
let x be FinSequence of U1; :: thesis: ( not x in dom O1 or h . (O1 . x) = O2 . K156(the carrier of U1,the carrier of U2,x,h) )
assume x in dom O1 ; :: thesis: h . (O1 . x) = O2 . K156(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, MSUALG_3:def 9;
A9: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 16;
Den o,((MSAlg U2) Over (MSSign U1)) = the Charact of ((MSAlg U2) Over (MSSign U1)) . o by MSUALG_1:def 11
.= (MSCharact U2) . o by A2, A9, Th9
.= O2 by A5, MSUALG_1:def 15 ;
hence h . (O1 . x) = O2 . K156(the carrier of U1,the carrier of U2,x,h) by A1, A7, A8, Th15; :: thesis: verum