let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for T being non-empty trivial MSAlgebra over S
for f being ManySortedFunction of A,T holds f is_homomorphism A,T
let A be non-empty MSAlgebra over S; :: thesis: for T being non-empty trivial MSAlgebra over S
for f being ManySortedFunction of A,T holds f is_homomorphism A,T
let T be non-empty trivial MSAlgebra over S; :: thesis: for f being ManySortedFunction of A,T holds f is_homomorphism A,T
let f be ManySortedFunction of A,T; :: thesis: f is_homomorphism A,T
let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,A) = {} or for b₁ being Element of Args (o,A) holds (f . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,T)) . (f # b₁) )
assume Args (o,A) <> {} ; :: thesis: for b₁ being Element of Args (o,A) holds (f . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,T)) . (f # b₁)
let x be Element of Args (o,A); :: thesis: (f . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,T)) . (f # x)
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then reconsider a = (Den (o,A)) . x as Element of the Sorts of A . (the_result_sort_of o) by FUNCT_1:13;
(Den (o,T)) . (f # x) in Result (o,T) ;
then ( the Sorts of T . (the_result_sort_of o) is trivial & (Den (o,T)) . (f # x) in the Sorts of T . (the_result_sort_of o) & (f . (the_result_sort_of o)) . a in the Sorts of T . (the_result_sort_of o) ) by A1, FUNCT_1:13;
hence (f . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,T)) . (f # x) by ZFMISC_1:def 10; :: thesis: verum