let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A
let A be MSAlgebra over S; :: thesis: for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A
let h1, h2 be Endomorphism of A; :: thesis: h2 ** h1 is Endomorphism of A
let o be OperSymbol of S; :: according to MSUALG_3:def 7,MSUALG_6:def 2 :: thesis: ( Args (o,A) = {} or for b₁ being Element of Args (o,A) holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,A)) . ((h2 ** h1) # b₁) )
assume A1: Args (o,A) <> {} ; :: thesis: for b₁ being Element of Args (o,A) holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,A)) . ((h2 ** h1) # b₁)
set h = h2 ** h1;
let x be Element of Args (o,A); :: thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x)
A2: Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3;
A3: h2 is_homomorphism A,A by Def2;
reconsider f1 = h1 . (the_result_sort_of o), f2 = h2 . (the_result_sort_of o), f = (h2 ** h1) . (the_result_sort_of o) as Function of ( the Sorts of A . (the_result_sort_of o)),( the Sorts of A . (the_result_sort_of o)) ;
A4: h1 is_homomorphism A,A by Def2;

per cases ( the Sorts of A . (the_result_sort_of o) = {} or the Sorts of A . (the_result_sort_of o) <> {} ) ;

suppose A5: the Sorts of A . (the_result_sort_of o) = {} ; :: thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x)

then dom f = {} ;
then A6: f . ((Den (o,A)) . x) = {} by FUNCT_1:def 2;
dom (Den (o,A)) = {} by A2, A5;
hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x) by A6, FUNCT_1:def 2; :: thesis: verum

end;

suppose A7: the Sorts of A . (the_result_sort_of o) <> {} ; :: thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x)

(h2 ** h1) . (the_result_sort_of o) = f2 * f1 by MSUALG_3:2;
then ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = f2 . (f1 . ((Den (o,A)) . x)) by A1, A2, A7, FUNCT_2:5, FUNCT_2:15
.= (h2 . (the_result_sort_of o)) . ((Den (o,A)) . (h1 # x)) by A4, A1
.= (Den (o,A)) . (h2 # (h1 # x)) by A3, A1 ;
hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x) by A1, Th5; :: thesis: verum

end;

end;