let S be non empty non void ManySortedSign ; :: thesis: for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
let U1, U2, U3 be non-empty MSAlgebra over S; :: thesis: for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
let H1 be ManySortedFunction of U1,U2; :: thesis: for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
let H2 be ManySortedFunction of U2,U3; :: thesis: ( H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 implies H2 ** H1 is_homomorphism U1,U3 )
assume that
A1: H1 is_homomorphism U1,U2 and
A2: H2 is_homomorphism U2,U3 ; :: thesis: H2 ** H1 is_homomorphism U1,U3
let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) )
assume Args (o,U1) <> {} ; :: thesis: for x being Element of Args (o,U1) holds ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x)
let x be Element of Args (o,U1); :: thesis: ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x)
set F = H2 ** H1;
set r = the_result_sort_of o;
(H1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (H1 # x) by A1;
then A3: (H2 . (the_result_sort_of o)) . ((H1 . (the_result_sort_of o)) . ((Den (o,U1)) . x)) = (Den (o,U3)) . (H2 # (H1 # x)) by A2;
A4: ( (H2 ** H1) . (the_result_sort_of o) = (H2 . (the_result_sort_of o)) * (H1 . (the_result_sort_of o)) & dom ((H2 ** H1) . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) ) by Th2, FUNCT_2:def 1;
rng the ResultSort of S c= the carrier of S by RELAT_1:def 19;
then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def 2;
then A5: ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def 5, RELAT_1:27;
o in the carrier' of S ;
then o in dom the ResultSort of S by FUNCT_2:def 1;
then Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A5, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;
then ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (H2 # (H1 # x)) by A3, A4, FUNCT_1:12;
hence ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) by Th8; :: thesis: verum