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
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 )
assume A1: U1,U2 are_similar ; :: thesis: ( 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) ; :: thesis: h is_homomorphism
thus U1,U2 are_similar by A1; :: according to ALG_1:def 1 :: thesis: for b₁ being set holds
( not b₁ in dom the charact of U1 or for b₂ being M17( the carrier of U1, Operations U1)
for b₃ being M17( 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₃ . K138( the carrier of U1, the carrier of U2,b₄,h) ) ) )
let n be Nat; :: thesis: ( not n in dom the charact of U1 or for b₁ being M17( the carrier of U1, Operations U1)
for b₂ being M17( 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₂ . K138( the carrier of U1, the carrier of U2,b₃,h) ) ) )
assume n in dom the charact of U1 ; :: thesis: for b₁ being M17( the carrier of U1, Operations U1)
for b₂ being M17( 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₂ . K138( 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 M17( 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₁ . K138( 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 . K138( 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 . K138( 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 . K138( the carrier of U1, the carrier of U2,x,h) )
assume x in dom O1 ; :: thesis: 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; :: thesis: verum