let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st h is_homomorphism holds
MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
let h be Function of U1,U2; :: thesis: ( h is_homomorphism implies MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) )
set f = MSAlg h;
set A = (MSAlg U2) Over (MSSign U1);
A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 11;
consider m being Nat such that
A2: the carrier' of (MSSign U1) = Seg m by MSUALG_1:def 7;
assume A3: h is_homomorphism ; :: thesis: MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
then A4: U1,U2 are_similar ;
then A5: MSSign U1 = MSSign U2 by Th10;
let o be OperSymbol of (MSSign U1); :: according to MSUALG_3:def 7 :: thesis: ( Args (o,(MSAlg U1)) = {} or for b₁ being Element of Args (o,(MSAlg U1)) holds ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . b₁) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # b₁) )
assume Args (o,(MSAlg U1)) <> {} ; :: thesis: for b₁ being Element of Args (o,(MSAlg U1)) holds ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . b₁) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # b₁)
o in Seg m by A2;
then reconsider k = o as Element of NAT ;
reconsider O2 = Den (o,((MSAlg U2) Over (MSSign U1))) as operation of U2 by A4, Lm2;
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 A5, A1, Th9
.= the charact of U2 . o by MSUALG_1:def 10 ;
then A6: O2 = the charact of U2 . k ;
set O1 = Den (o,(MSAlg U1));
let y be Element of Args (o,(MSAlg U1)); :: thesis: ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y)
A7: ( Den (o,(MSAlg U1)) = the charact of U1 . o & the carrier' of (MSSign U1) = dom (signature U1) ) by Th12, MSUALG_1:def 8;
reconsider O1 = Den (o,(MSAlg U1)) as operation of U1 by Th13;
A8: y is FinSequence of the carrier of U1 by Th14;
( dom (signature U1) = dom the charact of U1 & Args (o,(MSAlg U1)) = dom O1 ) by Lm1, FUNCT_2:def 1;
then h . (O1 . y) = O2 . (h * y) by A3, A7, A6, A8
.= (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y) by A4, Th15 ;
hence ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y) by A4, Th11; :: thesis: verum