let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being MSAlgebra over S st A2 is empty holds
for h being ManySortedFunction of A1,A2 holds h is_homomorphism A1,A2
let A1, A2 be MSAlgebra over S; :: thesis: ( A2 is empty implies for h being ManySortedFunction of A1,A2 holds h is_homomorphism A1,A2 )
assume A1: the Sorts of A2 is empty-yielding ; :: according to CATALG_1:def 2 :: thesis: for h being ManySortedFunction of A1,A2 holds h is_homomorphism A1,A2
let h be ManySortedFunction of A1,A2; :: thesis: h is_homomorphism A1,A2
let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,A1) = {} or for b₁ being Element of Args (o,A1) holds (h . (the_result_sort_of o)) . ((Den (o,A1)) . b₁) = (Den (o,A2)) . (h # b₁) )
assume Args (o,A1) <> {} ; :: thesis: for b₁ being Element of Args (o,A1) holds (h . (the_result_sort_of o)) . ((Den (o,A1)) . b₁) = (Den (o,A2)) . (h # b₁)
let x be Element of Args (o,A1); :: thesis: (h . (the_result_sort_of o)) . ((Den (o,A1)) . x) = (Den (o,A2)) . (h # x)
the Sorts of A2 . (the_result_sort_of o) = {} by A1;
then A2: Result (o,A2) = {} by PRALG_2:3;
thus (h . (the_result_sort_of o)) . ((Den (o,A1)) . x) = {} by A1
.= (Den (o,A2)) . (h # x) by A2 ; :: thesis: verum