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