let U1, U2 be Universal_Algebra; 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; ( 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
; 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); MSUALG_3:def 7 ( Args (o,(MSAlg U1)) = {} or for b1 being Element of Args (o,(MSAlg U1)) holds ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . b1) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # b1) )
assume
Args (o,(MSAlg U1)) <> {}
; for b1 being Element of Args (o,(MSAlg U1)) holds ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . b1) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # b1)
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)); ((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; verum